- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5717170a-a5a7-47ff-af47-0e6fee4329bf
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 25
    column: 10
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 253b8e00-74dd-4b27-82cd-61aa17029b0a
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 25
    column: 10
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc059380-a0be-4d2e-89a6-2a3b6a287020
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 28
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b35ac26-7589-45eb-9dd0-aefe56a0071e
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e1d28a1-8c60-4178-9e31-921db3fc6637
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61ad366f-7fea-486a-9431-b0c8d92d3f95
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 30
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 652975c4-3317-499f-93c8-ade70de2adf9
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbd98926-9bf3-4a56-b7ef-0434dc0bff26
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1bbb0d8-56c1-4613-a137-5e284b0ed418
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d99ad2f8-926f-42e8-9b32-45a77c55a401
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f5c3e9c-3a4a-4f6d-bc70-eb94f1e69fd5
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c44eb662-52de-4557-a7c7-f8e21ff4fc98
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72d0d87a-9d52-45ea-bb00-794be0af7618
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82ff2f81-7a48-4750-a441-1e87592db0fc
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 665cc505-313a-41bd-a427-70fd8dfe3469
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 17
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d367f82-2733-4e6f-a1c4-0100e6411ab4
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 17
    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: 0aaffec2-db28-4ffc-836b-fa304a19cc86
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 17
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10ffcb9c-82cd-45f8-b91a-8c49d5da9a19
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 17
    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: f3726a9d-6bcc-46c7-8c8c-5715dd844707
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 19
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ad4d15d-56f1-4484-88b1-a6808c2c5a72
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 19
    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: 8797f25f-ef34-42ea-8c63-7f68a4c5b08f
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 19
    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: 88c512b8-70c9-4df5-ab97-1ef6b5e88fbb
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 19
    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: f402ab7a-01dd-4306-97a3-21df8bee24e3
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 22
    column: 7
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b570a80-9c1e-4f93-b183-463cfb3bc5ed
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 22
    column: 7
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3719c185-edb2-41df-baac-ea49e684d0d9
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 24
    column: 10
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0638e87-050c-410c-a97e-617c3fa5b7f5
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 24
    column: 10
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ca8031c-bf25-41de-a3b3-36fd49c18358
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 21
    column: 5
    function: main
  loop_invariant:
    string: j <= 1U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c43ec55d-a13b-4db5-b1dc-c32ee237cd3c
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 21
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3ba647a-8578-465e-9d1c-694678fc6ca5
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 21
    column: 5
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a5664d1-c2d6-4841-ab29-769c60cb9002
    creation_time: 2023-01-27T16:29:17Z
    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/array-1.c'''
    task:
      input_files:
      - ../plain/array-1.c
      input_file_hashes:
        ../plain/array-1.c: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array-1.c
    file_hash: 229f3e8ce4e3b13e76b58dc42b5f9a4638bd79f9f3aa927499d1d902ea457152
    line: 21
    column: 5
    function: main
  loop_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
