- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1f21b9b-962f-4c17-af2c-1629dd0d4ad7
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 31
    column: 4
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 323b4d89-cfb0-4a90-8560-1b91ee515575
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c8edb42-79fe-497c-acb5-d4de8714d8bc
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a524817-ab47-4ed0-9a35-9090e10b872c
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19282bc8-64e6-42a6-b85e-c079974bc0f3
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 32
    column: 8
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc505f1a-c2fa-4927-9ed4-b10b568d7c6c
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de08d044-911f-42ea-9b84-e82f5f4ecd28
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 32
    column: 8
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6bf2a79-3f97-410f-8e61-0e983c25e4df
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 32
    column: 8
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c437112-6d42-435d-8644-c94f1d5f9968
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 32
    column: 28
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b9cd5bd-c3b1-4499-bb74-ae968337c535
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 32
    column: 28
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8133db82-90fc-43ee-8954-0c976680ef3f
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 32
    column: 28
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afe64079-e78e-4c1a-a9ee-104fb1bf532d
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 35
    column: 4
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6a79d72-d880-4ad6-a7f1-3a6f733a7cd4
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffb61404-3929-40e3-9ef4-6be1e82272f9
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d324a4c-eeb8-41ef-bda2-d2e725d5e749
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f90f35c-01bc-4e77-bd22-72130cfa6377
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 36
    column: 7
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a186f587-f5d5-47aa-9264-aef5aa9902d3
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 36
    column: 7
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b848dc04-7860-4960-a86c-773a4d5f11da
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 36
    column: 7
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08ed7d07-e734-417a-b839-8f692e606d53
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 36
    column: 7
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9173102-2457-4f62-a67d-f23b12cb7c51
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 36
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0096ec3c-f6fb-4fd0-8d62-677c260aae5b
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 36
    column: 27
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e7d4b3a-21f0-4746-8756-c81589f2f74b
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 36
    column: 27
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 075e9d20-6e84-4195-90e3-e609166e51d8
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 39
    column: 5
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab7a6e1f-215d-41c9-a069-9bcddfb1b521
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02910d1c-26a7-45f3-afdb-a06c22b2e527
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 39
    column: 5
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd85861d-06ea-43f3-bdc6-295ca3c72c5c
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 39
    column: 5
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ae2de43-97a8-46a5-9d18-6ee36e61e69d
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 41
    column: 5
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51e26012-7321-43dd-8a85-9e2a0162185c
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 41
    column: 5
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b294e21f-d6fd-4294-b9da-fbce304617f0
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 41
    column: 5
    function: main
  location_invariant:
    string: (-1LL + (long long )M) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bc56aba-61a3-4385-a95a-ec3f98fb3d33
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 41
    column: 5
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7539501f-b564-4a8d-aca3-9930ee6bd673
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 42
    column: 0
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8bd6310-7c82-45f3-9168-5159ed330aff
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 42
    column: 0
    function: main
  location_invariant:
    string: (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fd9863b-03cf-4888-aeed-70c2a160deba
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 27
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9fb0379-50e5-46af-9456-08ed9b0c7bd9
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 27
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2d631b9-b53f-41f8-833f-996fbaad8c52
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 27
    column: 15
    function: main
  location_invariant:
    string: (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26817489-eb11-4d9e-a33d-44e87c9e27c0
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 27
    column: 15
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14b97491-3f3a-4c0c-977c-8eda4661614a
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8557c48-550c-49bb-9294-f0d7d7b23e8b
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5de193b2-4ca8-4813-b389-6dc7eed2d3fd
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 6
    function: main
  location_invariant:
    string: (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b4f4a07-d201-4401-902b-e171874efb8b
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f39eb975-38d5-494a-bb10-2c28d8949ded
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd8bb538-36d9-4724-998f-abcc2bb0b8f0
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 207ed61e-35f7-428c-9da8-8b4c69c2f545
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 12
    function: main
  location_invariant:
    string: (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6232e07-594b-46e7-9742-7d903651a192
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 12
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f879ecf-3179-4f57-aca3-b005257a34c8
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 18
    function: main
  location_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cd4554c-058a-4900-9712-9b7de58e0cda
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 18
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b0de892-8acb-4004-8d76-19368dca6398
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 18
    function: main
  location_invariant:
    string: (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7a61094-cbef-423f-bfb2-6701d60c4676
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 28
    column: 18
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e46b87c-d3e2-44d0-85c9-e753803e6ef4
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 30
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e2728b4-70d6-4411-99e2-b8b231506234
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 30
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40e2642c-59a0-4ed8-905c-5abe2affe8b0
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 30
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e67dbfd-0c2b-42a3-9415-b639ea2f17d3
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f2656946-43c1-45ba-9a19-77c7a1c9e97d
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a016deae-db07-4016-a074-7b871b2aed1b
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 369a8592-9f03-4a68-bc16-60600039f812
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 38
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 787bfb0e-59a1-4af5-9113-872e0733e8f9
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 38
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e208cb80-e7ee-4a37-966b-3b3942e9bf04
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 38
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: edbdd5c0-f1a6-49ff-af82-44d7a280a682
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 40
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b8793b87-3159-4466-a5f5-28cfef831418
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 40
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 60c4be0e-eac0-4c80-85a5-ef62f4b9f60f
    creation_time: 2023-01-27T16:31:07Z
    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/sum_array-2.i'''
    task:
      input_files:
      - ../plain/sum_array-2.i
      input_file_hashes:
        ../plain/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 40
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
