- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c57fae0-35be-4c34-b21d-4f08d9b7432a
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    column: 6
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cec4b0bb-049a-4649-9b9c-be1b1a2a258e
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    column: 6
    function: main
  location_invariant:
    string: 1 <= nlen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d2f4787-9978-42d8-8b95-72d72b25d727
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    column: 6
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98efcad2-60cf-4833-bfaf-a145b541dd29
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    column: 6
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22209c7e-13b6-4042-9691-2e5fb3621280
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    column: 6
    function: main
  location_invariant:
    string: 7LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cef00566-d449-4575-b1a6-246b9dbcdbca
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    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: 662c7496-8dd9-442d-a557-1bdef3779db5
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a882b2d7-cecd-445c-94ab-c0bbb7cd5310
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 29
    column: 6
    function: main
  location_invariant:
    string: nlen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cf6bc9f-be26-4e46-8938-affafd57e374
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    column: 6
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e37dcec6-6aa8-4b8a-896f-c106cd309c3e
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    column: 6
    function: main
  location_invariant:
    string: 1 <= nlen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2ea12e7-f9c2-4573-b6bd-7d84832403a1
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    column: 6
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24d7cbb4-26c4-4d93-a7f1-98897fdcbac7
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    column: 6
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b68f220e-310e-4ada-9029-984271451282
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    column: 6
    function: main
  location_invariant:
    string: 7LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aee4ef2e-1c2b-42b4-8064-401cd7e582df
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    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: e1ffeff2-568c-43cb-bd6d-c896edf0d127
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07950759-9184-450f-b1fc-d6e42224254d
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 30
    column: 6
    function: main
  location_invariant:
    string: nlen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a2f402e-bf5c-4654-a6a0-e7de5a3a5b4e
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 33
    column: 2
    function: main
  location_invariant:
    string: (long long )i - (long long )nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72cd03b0-64a5-4ef3-b27d-df5be5101035
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 33
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 714a5283-5ef0-4964-8edc-ce98e1658581
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 27
    column: 6
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4378642e-a316-4b70-8b54-daa96298004c
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 27
    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: 635db5ac-6a98-4880-adc6-4ddf3af92e2c
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 73125804-8fca-42c1-8c4e-02987ffb00c4
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d24ce1c-5604-48ae-bdb0-f5f11fc49522
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: 1 <= nlen
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fdeb885-fe11-4d82-9f8e-3d36ef247067
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b81975a0-667d-4c37-bac3-3081b3b42fc1
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: j <= 8
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c815a26-cff0-4c03-8811-dfff41cb718a
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: (-1LL - (long long )i) + (long long )nlen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 09e158b6-ee39-46c3-9a66-6f6ee9710488
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: 8LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d5b6b98-d1b4-4a4b-b92f-b286a93cd9cd
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b91b704-8973-4806-8ad4-e3ff95061055
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 116d2cae-3ca9-43e8-9bda-e01870a3ca70
    creation_time: 2023-01-27T16:29:39Z
    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/id_build.i'''
    task:
      input_files:
      - ../plain/id_build.i
      input_file_hashes:
        ../plain/id_build.i: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i
    file_hash: 2c4c8975bee6324b0c0486aa99ba8be369d6762a33e8dd5b012191d5fa43c106
    line: 28
    column: 8
    function: main
  loop_invariant:
    string: nlen != 0
    type: assertion
    format: C
