- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48eaa094-68fd-43f9-844a-517991e001aa
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ba15b3c-74f1-47a5-bb99-76f28f109c93
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 30
    column: 4
    function: main
  location_invariant:
    string: i <= 2047
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de67a0be-4606-405d-8c7a-5475e438fa88
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 2047LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8aca6ef-2442-4d67-884b-c4801ed19188
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 30
    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: 4b1aef26-33c3-49d7-91b7-463613329697
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a2a4c80-c08c-488f-9923-336425b52c32
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 31
    column: 4
    function: main
  location_invariant:
    string: i <= 2047
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: debeb553-c8db-401a-a1bf-393e448f2d9f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 2047LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffdfc98c-e329-4b05-a774-dd4220d705e6
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    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: c2afeee5-5c27-4350-b1a6-e7e67ccbccc0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 33
    column: 2
    function: main
  location_invariant:
    string: -2048LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea5d2f53-03dd-47f1-b356-165180d451dc
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 34
    column: 0
    function: main
  location_invariant:
    string: -2048LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5231a1b3-db07-4c01-add6-205a025e3936
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e38119f7-9249-4f7b-8c0b-de09b51378cf
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 26
    column: 4
    function: main
  location_invariant:
    string: i <= 2047
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fd30715-33a7-490b-8c62-52fe4e4ac7d7
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 2047LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f80688b5-26d0-48e7-875d-7e6e58163ba9
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 26
    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: fe92aeab-d430-4248-8ba8-ebefc4b88005
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bdbbb14-91f2-4232-a9bb-23256a48d417
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 27
    column: 4
    function: main
  location_invariant:
    string: i <= 2047
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b80672d6-f12d-4736-b5ff-3a7bfbd58c34
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 2047LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ff51e3e-4af5-4601-b052-83b54f6d3e54
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5baff1e0-b631-492b-91a7-845b82290635
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 29
    column: 6
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 878790dc-63af-4efd-bacc-b7e3da494019
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 29
    column: 6
    function: main
  loop_invariant:
    string: i <= 2048
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 39073656-968b-4493-852b-478828c036a1
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 29
    column: 6
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c53686d8-b6c3-422b-b067-138cbd815aa0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cc9966a8-99bb-4753-84fd-0b4fb44ee6ca
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: i <= 2048
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d4071210-28c6-434b-93ac-47f9a0cd9327
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/array_2-2.i'''
    task:
      input_files:
      - ../plain/array_2-2.i
      input_file_hashes:
        ../plain/array_2-2.i: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/array_2-2.i
    file_hash: 866342b97e5be917007cb97e07a0644c7c9d2aa9b428c32cf026d727d672a191
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
