- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f99c2fd-a74b-498c-84de-7a6c3345c9c1
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4575dc8-4492-411d-b3f5-80050e9b26d2
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 23
    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: 588ccbbc-bf45-47f6-bff5-7c71e34d6a9d
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 24
    column: 4
    function: main
  location_invariant:
    string: i <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b142ee6-70b6-472e-b91b-f8af3da17e8a
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9774cfc3-b3b5-4fd4-add1-8842e174a888
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 24
    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: 9a8c7af8-300c-4b73-8ab7-298cb8f5f873
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 26
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1824cda-6029-4805-842d-e5df31ecd6c7
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 26
    column: 6
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6aed5d08-5d9f-46c7-a353-ca3e79259ff9
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 28
    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: 249c17fd-80ee-4215-afb8-9e153b42154c
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01a7494b-e361-496b-96a0-1b5cc86a8a29
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39250af8-204e-4605-b5d9-fd3f38210dd2
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 29
    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: c321c393-34c6-4386-af0f-87deea6e617a
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4cb7679-c7de-4cde-ab55-aa1d3b801b04
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e543d11-ada3-45f1-b652-1c3b3718b316
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 100e4921-0dce-432f-9c9c-e6b7f53f76c5
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 30
    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: adc062d5-5aff-490d-b6b5-eac281900751
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19b6a526-5616-486e-b0d8-77a091f333ac
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9545289-82ec-479a-b861-ab5e4173a3b2
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 32
    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: c667e5e7-2816-414f-801b-a91ccfcfaa34
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 32
    column: 2
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3da02c0a-d52b-4a13-8565-42108e5e5683
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 32
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7bd565f-f1aa-4381-99ad-e9816451411f
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: 4294967295LL - (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adeacd98-e1b0-42f4-af33-fd33ed0bc253
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db722ea3-ea6b-4eb7-b765-9d40c3e6150c
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 18
    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: f477b140-1c31-4254-93d8-96b79c2b7745
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0061ee1-1489-4dd1-977b-327b52c1cfe5
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b742e45d-adfa-432b-8771-12c55a828f53
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 18
    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: 09440e80-1856-4475-baa6-95432f7a97b5
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4dd510cf-40e4-470e-93ba-28a6c5f06899
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95a8e875-f51a-4b29-974c-17f8a610fc75
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da7360eb-a0c7-478f-9237-da5ea7666fd1
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ace5b4df-db49-40f2-a279-cbe60991ced5
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81a33315-348f-43ea-ad5a-e4c7d563097a
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 493ef092-25bf-4963-b44c-539b93a11283
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6928ebf9-bf7c-447b-afa6-81527d0fb8d1
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5711f8de-c419-43d2-8ecd-b1d4e8426eec
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    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: bf7ce5c9-88e9-44c5-ae1c-fafb899b378d
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2714ab00-93af-4607-b74d-5cbfd44d675d
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8197b03-bc89-4b7d-9eda-24388a5e608b
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    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: 5f4ffe1d-7fd4-4499-bcdf-e70f12440e2d
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 20
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af2bf9d1-1d06-4c1b-ab0c-945e4d9251f3
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 19
    column: 20
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8945cc37-b2bf-4464-b5fc-f330751834ba
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13d24d86-582f-4eac-9702-b5bb268bcd5f
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 20
    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: d130772b-483a-42fc-94ed-93ce22c0c34e
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b69ba35e-3f3a-4a7c-af08-dd066ec6410d
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1b30b52-0f7b-4689-b425-56f55cf7b9e3
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 20
    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: 4f3ee07e-f012-4ba6-baeb-b7f7f4d6d039
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a70bc5c-ceb5-4109-b3cf-b95f868f5102
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6cceb426-65fd-41a2-b5a5-8b52d7023384
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 21
    column: 2
    function: main
  location_invariant:
    string: k <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a57983ef-ec00-409d-8022-5f3878f23dae
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a9e39d5-1a78-40e5-a71e-22861a21099b
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed386898-d111-4c60-921b-0fd572e83550
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50297c84-f09f-4cfc-a1ec-06dd60d01aaf
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e60b79a3-c8eb-4f03-89d1-6abcf5442fe6
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1433d3a6-16ef-4f1c-8653-9174c84b1626
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: i <= 20000003U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e61fe2f0-b8bd-455a-8ff5-dda490257985
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1662ec5b-adb4-4768-8440-cede7b1934fe
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 27
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 55d98e58-297b-4353-b6bd-c94a10e6b4ac
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 27
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 47c08a94-f731-4e94-80bf-594073962c63
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 27
    column: 9
    function: main
  loop_invariant:
    string: i <= 20000003U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 947d9524-7176-4b5b-a56e-775aa86df079
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 27
    column: 9
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e75f1b13-20d4-4043-9039-4e52cb83aa76
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 27
    column: 9
    function: main
  loop_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 20c477c3-3a5a-4be6-8cd7-dff50fffab2b
    creation_time: 2023-01-27T16:31:10Z
    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/vnew1.c'''
    task:
      input_files:
      - ../plain/vnew1.c
      input_file_hashes:
        ../plain/vnew1.c: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vnew1.c
    file_hash: 92c9725cc4c9709a9ab81826fb3481ef81541ab6f68244b6727f50e97bc0f0c0
    line: 27
    column: 9
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
