- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 574be8ce-0edd-4f07-8b30-e5774f18b474
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 20
    column: 6
    function: main
  location_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb5b88e1-9442-4222-a170-002fb95563e7
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 20
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a7685de-61a7-4a62-85b2-c1a2b2e5d2a0
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 20
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9dcefe6-8acb-41de-97c3-114759e84db7
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 20
    column: 6
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0176191e-3165-4ff1-9d2d-08f26312eeac
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 21
    column: 6
    function: main
  location_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6314735d-bfad-47b4-9aa1-44f55ef542a2
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 21
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77c4937a-5169-4575-a03c-eae6a80872f2
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 21
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cdfddafe-2cee-489a-bc98-e5ee9acf6159
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 21
    column: 6
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36c29eea-7d51-4d5e-90fd-f42040a92c50
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 23
    column: 9
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 526fe81f-c414-4fe5-8090-b3fd3eb942eb
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 23
    column: 9
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e845268c-33a0-4656-b391-c735c607880f
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 23
    column: 9
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35f8f824-2350-445f-83ef-9233f15c9ed3
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 23
    column: 9
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ffea467-59d6-4fac-96c1-69a8f53f5090
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 23
    column: 9
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab6887a0-5f82-425e-bedf-af464bcbbc3b
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 23
    column: 9
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57361824-4d6a-4abf-a441-63a756dd74f7
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 24
    column: 9
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46c62463-a04d-481e-bcf2-1cd2f4c5f4eb
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 24
    column: 9
    function: main
  location_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3ffa22e-05d4-4b45-a0d5-e452f0bc8c68
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 24
    column: 9
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9d3d495-4962-4a89-855f-3a59989ba8e3
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 24
    column: 9
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64d11b21-2b93-41eb-acf1-bba75c390c4f
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 24
    column: 9
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a521397-e6d8-41f6-835c-779c1f59799b
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 24
    column: 9
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02ab1c67-fa2c-4809-abde-1d9f801cfc41
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 24
    column: 9
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e3d7dd5-f9c4-4bb2-bc31-155bb8245704
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 26
    column: 6
    function: main
  location_invariant:
    string: -1 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33e4c2d9-22f3-478c-9ff4-666bc641ebc3
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 26
    column: 6
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf66c969-2dab-483c-a00b-cc2d557aae28
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 26
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 594ce61d-319e-4962-900a-43353d875598
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 26
    column: 6
    function: main
  location_invariant:
    string: 1LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f8580bb-9f7d-4e44-a628-3ca7b3540817
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 26
    column: 6
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d561fb69-4b6a-4667-a4ec-49d6d2e3826c
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 26
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b641b091-4251-412a-9ccf-a90322d2ed20
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 26
    column: 6
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44d8dbc3-2d25-4e64-9d82-2dd38c021faa
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 1 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 629519e8-915c-4666-851f-67e267054aa4
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 29
    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: 467b23f0-32bf-4e14-9d8e-15e4299caad8
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a438ad2-7fad-44d7-b97d-9bd3a85899f5
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c542d9d-5bc0-4915-927d-7fc4a46e30d7
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b450a988-64a3-4814-9037-b89895ebe3e5
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 30
    column: 3
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a28712a9-0587-4cef-ae38-f186d7a77db5
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 30
    column: 3
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ef68673-c6b7-4752-b69c-9f9c5cee2800
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 30
    column: 3
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93296302-1ba1-4a47-945b-fbd3416a0241
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 30
    column: 3
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d3a59bc-8ef4-4b47-b86c-f79a507f5815
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 14
    column: 16
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 573712f5-967e-44c1-a62a-6a179f51adc5
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 14
    column: 16
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75afc678-7ece-40f2-85e6-d0f1c3bab63f
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 16
    column: 7
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 607be99d-196f-440d-a125-eee2a0f6d07b
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 16
    column: 7
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd303655-2946-4f8d-b454-cd34c63b4135
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 18
    column: 6
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6843fd6b-a910-43cd-b498-3c1704547137
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 18
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f957916-9619-47d8-9e0b-74231166cc27
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 18
    column: 6
    function: main
  location_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1566e8f3-9bb5-4711-85ce-364cc0550585
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 18
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a4dca1c-b54d-4670-8fb7-bf8dbe786079
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 19
    column: 7
    function: main
  loop_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c3613d8-41a1-40e6-bbb5-0ea681dc0fa1
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 19
    column: 7
    function: main
  loop_invariant:
    string: SIZE <= 2147483647U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 54a5edec-4bd7-4aa2-b484-416196375307
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 19
    column: 7
    function: main
  loop_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ac6fa521-d2f1-4bc6-bc15-0855e9bb6919
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 19
    column: 7
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c96ede5e-2cf8-41e8-9dc0-83f4aac5d3d6
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 19
    column: 7
    function: main
  loop_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dd7307d-e4b6-48e3-8d82-86f891f1efff
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: -1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 71000bf9-6639-4d39-88da-3b5a58b65b3a
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 25aa0386-5f59-4b6f-a596-6e1b7c4afab6
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: 2U <= SIZE
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 86e466be-4efe-4ec3-bfe4-13bc8895e0cd
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: SIZE <= 2147483647U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c49c01b9-05bf-4ff8-aadd-65fc266e2e11
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f7f7bb9-0a94-4371-b7fa-2e3381d91130
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2924e84c-8c7e-4af4-989b-767041ff600b
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: 1LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1136f531-42ac-4af4-981c-48e95b185bf9
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: (-1LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cdff00e-f6da-4b3e-afe4-9acf2ca66883
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a26ceaa-b658-4896-ab64-061ccecf2da2
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b43ce20a-c9f9-4c9f-adc6-42e6882bbdfd
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 22
    column: 13
    function: main
  loop_invariant:
    string: SIZE != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 55e856e8-6332-419e-918d-1a518c202681
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 28
    column: 6
    function: main
  loop_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8530f220-8b21-4b89-a266-ba3ef42cb47b
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 28
    column: 6
    function: main
  loop_invariant:
    string: 1 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 95b5c2ac-954e-41ae-a0d8-1af89892df12
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 28
    column: 6
    function: main
  loop_invariant:
    string: SIZE <= 2147483647U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e3dd8645-2eef-49ea-aada-eef96c30bffa
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 28
    column: 6
    function: main
  loop_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4120d458-2c8d-4197-9294-be858b744bdf
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 28
    column: 6
    function: main
  loop_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9021a46c-4776-4f74-a4c3-28c5471ce9b8
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 28
    column: 6
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f4217496-74d5-41e0-b9ff-a815cf19b297
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 28
    column: 6
    function: main
  loop_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41b7b0b1-729e-4a18-b3a8-697bc2d282ed
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d5bf3b0-ab9d-4fd5-8079-e98905c16d1c
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 61390fa1-94df-42c8-8492-f501a9be260f
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: (long long )SIZE >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 78378c5d-e9cd-43e1-aef2-cf801dea3d89
    creation_time: 2023-01-27T16:29:40Z
    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/insertion_sort-2.c'''
    task:
      input_files:
      - ../plain/insertion_sort-2.c
      input_file_hashes:
        ../plain/insertion_sort-2.c: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/insertion_sort-2.c
    file_hash: e6909fdbd47ee7cc9ac1cfcb139a86d0e022eb1f9eab8a625d6818fa3999b29d
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
