- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13c282c5-a699-4219-9bfc-53b8f6f2b37f
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 30
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a54d0d96-b09f-4144-8390-988c0bb89304
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 30
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08400559-3eaf-471d-9d48-592abee70382
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 32
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f1a59da-ff21-41a4-9691-08d1c49ad4fc
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 32
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2088c80a-1803-4f83-9312-218e7bb9e649
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )N_LIN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bba3a968-b246-49de-b644-da246eb47fcb
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )N_COL >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd183617-55a9-4ed6-bf20-10778ad46360
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    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: 0fdb3bfc-6463-4cfd-8751-121caff89d7c
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    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: a7f2d5f9-36a1-40a2-9960-90d7efb42f98
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )N_LIN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f03f5b73-90c5-42f9-a322-d471b56774dc
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )N_COL >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 447f2ecf-a425-4b73-9e95-2dc2f8bf8f7f
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    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: e60b647f-4a43-4c7c-b4ae-9a823bcde1ed
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    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: 3319b97b-c9d5-4b5c-92e5-41602cc80d8f
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )N_COL >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ea0b469-19eb-4c0f-a9ad-bc2910fa3a31
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 16
    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: 2a97c671-f2f7-4da8-a6c8-a96f252bb2ec
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 16
    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: 6e205dfd-575e-48fd-85a2-e67e9e8d5fff
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )N_COL >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 238020a8-3175-4c94-81e9-ff9f03e22ac4
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 16
    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: 4f9842f6-600d-4748-ab6b-53ee386f009c
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 16
    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: f6c8102d-7e1c-4d79-921b-e86d943af8a8
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 18
    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: ae81a85f-d755-4217-967a-7bde9c7166a8
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 18
    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: 3671ca94-278c-4259-9115-cc157e11ed01
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 18
    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: 076c4638-c582-4e79-86ed-8bdc9ba6141e
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 18
    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: 590bad8c-ca63-4b0e-b1e0-0f2925cd96f1
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 20
    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: 65dd24cd-6118-484b-9946-4fae971bf5c7
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    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: 6e3c316d-e2fb-4f48-862b-d99c2be29ec5
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 20
    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: 3540fc15-74a0-401a-b8a0-ff7d9fa69889
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 20
    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: e5c8eb1f-c928-4893-a8ca-72bcb359707d
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 22
    column: 7
    function: main
  loop_invariant:
    string: k <= 1U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2982c2bd-9dbb-4fcc-b0ae-8201f16d1a60
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 22
    column: 7
    function: main
  loop_invariant:
    string: 1LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6db6dc4e-6cba-48e9-9635-b7ff187f3ec1
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 22
    column: 7
    function: main
  loop_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7dbac788-5b41-473d-8b7d-00c6da89a240
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    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: b449eac4-1387-4f89-b65c-771bc84a16d4
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 21
    column: 5
    function: main
  loop_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bf3674ba-6788-4a66-a289-6c341e1176a1
    creation_time: 2023-01-27T16:29:43Z
    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/matrix-1.c'''
    task:
      input_files:
      - ../plain/matrix-1.c
      input_file_hashes:
        ../plain/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/matrix-1.c
    file_hash: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
    line: 21
    column: 5
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
