- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce29fce1-f5ff-4da1-930b-93b239c3016f
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 34
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5127e9a-778a-4b0c-8406-42989dca06e0
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 34
    column: 2
    function: main
  location_invariant:
    string: 2147483646LL - (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7546a037-0607-496f-a59b-20ad1805a483
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 35
    column: 2
    function: main
  location_invariant:
    string: 1 <= MAXPATHLEN
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 851ccd43-3cf1-4209-8cf6-d80263290c07
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 35
    column: 2
    function: main
  location_invariant:
    string: MAXPATHLEN <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 172f168a-9252-4483-94d1-b59d97da55c6
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 35
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c02aa6bf-061e-46e9-a800-9b1a4d98d79c
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 35
    column: 2
    function: main
  location_invariant:
    string: 2147483646LL - (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c72a8bb9-1118-413a-8826-0bf8d230087b
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 35
    column: 2
    function: main
  location_invariant:
    string: MAXPATHLEN != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19277a1f-dc1f-4357-b66a-691d7d4a24a6
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 36
    column: 2
    function: main
  location_invariant:
    string: 1 <= bound_off
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce6ea85a-985c-446c-a115-bc53a3bb0502
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 36
    column: 2
    function: main
  location_invariant:
    string: bound_off <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e78b8c8d-fbb5-49de-ade6-130864a7983c
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 36
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ecbaaa5-6312-42e4-b6d4-f314945ff876
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 36
    column: 2
    function: main
  location_invariant:
    string: 2147483646LL - (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30f046a7-20a6-4b67-b912-b18a3a5e1abc
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 36
    column: 2
    function: main
  location_invariant:
    string: bound_off != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95af6866-a215-45c7-8517-5abdc3d500b3
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 37
    column: 2
    function: main
  location_invariant:
    string: 1 <= bound_off
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6dc13e4c-2d81-419c-8877-400c836ed300
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 37
    column: 2
    function: main
  location_invariant:
    string: bound_off <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acc2fc20-ab99-4869-918e-357078e553aa
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 37
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1031856f-1edf-4e16-8ecd-6b5f7eee662a
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 37
    column: 2
    function: main
  location_invariant:
    string: 2147483646LL - (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e67a31a-d2c8-48a2-ba64-ade7218cf130
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 37
    column: 2
    function: main
  location_invariant:
    string: bound_off != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3a15ce9-015f-44e5-8346-b148e5e1a6b5
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 41
    column: 4
    function: main
  location_invariant:
    string: 0 <= glob2_p_off
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fe3d6a3-8b88-4fb2-9b0c-7fe494a4e169
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 41
    column: 4
    function: main
  location_invariant:
    string: glob2_p_off <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d421fbc5-599b-4ec8-8342-3de71afc0d85
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 41
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd8c2b3d-beb2-46e8-8591-ad74f2dcfeb4
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 41
    column: 4
    function: main
  location_invariant:
    string: 2147483646LL - (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba7551bc-9497-426e-b5f3-d21661cb51f5
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 41
    column: 4
    function: main
  location_invariant:
    string: (long long )MAXPATHLEN - (long long )glob2_p_off >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 971a3928-8849-4695-b2e4-79249f0be8dd
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 41
    column: 4
    function: main
  location_invariant:
    string: (long long )glob2_p_off >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84e0b237-4472-44ae-8919-b9870a874f98
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: 0 <= glob2_p_off
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e773b8b-1058-403b-b703-c9d18feda595
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: 1 <= MAXPATHLEN
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 832c0200-cd94-4c26-9fe8-d02ebb223dc5
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: MAXPATHLEN <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1db6623d-ab0a-4f4e-a58b-1e35109cdd1c
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: glob2_p_off <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 611c86c0-471a-467b-8df9-4461155f0492
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25971c82-1c98-460c-99cf-faf2c95bde54
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: 2147483646LL - (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10c1bf38-6c3b-4af6-af50-f194ae5d6874
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: (long long )MAXPATHLEN - (long long )glob2_p_off >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24ba2fd0-d0d6-4154-b353-95361ec5eb14
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: (long long )glob2_p_off >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82226fb9-eab4-43ea-a25e-429edaad2170
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 42
    column: 4
    function: main
  location_invariant:
    string: MAXPATHLEN != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f13af4d2-4afa-41b1-949e-dd5bece98105
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 1 <= MAXPATHLEN
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63370884-a4cf-4b4c-882c-949c985048f3
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 33
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8572c862-db8e-4f2c-b036-5192d9814462
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 33
    column: 5
    function: main
  location_invariant:
    string: MAXPATHLEN != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: edcb43a3-d117-4f58-b26f-04c7e0de4444
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: 0 <= glob2_p_off
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f5a08e32-87c4-4af9-b1b8-a78a0eb875e3
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: 1 <= MAXPATHLEN
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f5ca2db4-cd79-4a15-9876-d30a6fde64f7
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: 1 <= bound_off
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c8c8bbc-820e-484f-8f44-3f1fb43c7a7e
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: 1 <= glob2_pathlim_off
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b19c78f4-53a0-4084-a573-ca49f6ef78ed
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: MAXPATHLEN <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fb407aa-de03-4b43-af2c-80bfe4aefb4d
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: bound_off <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f1cc0c5-9c1a-49f0-9224-ad868dc9baf5
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: glob2_pathlim_off <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cb661095-8b43-432d-bde6-067b9355b17e
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: -1LL + (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 561e5cc7-1528-426f-bf6c-576a62bd9c74
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: 2147483646LL - (long long )MAXPATHLEN >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d22e851d-315b-4d04-80af-a2dfdc8f76a7
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: (long long )glob2_p_off >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fff0c72e-7807-4228-b08a-f1204d4c9158
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: MAXPATHLEN != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 66b99cfb-851f-4deb-ad4d-08220d5f1829
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: bound_off != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f5ee9cbe-a384-41a6-8a55-c2883365f470
    creation_time: 2023-01-27T16:29:15Z
    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/NetBSD_loop.i'''
    task:
      input_files:
      - ../plain/NetBSD_loop.i
      input_file_hashes:
        ../plain/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: glob2_pathlim_off != 0
    type: assertion
    format: C
