- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ea37d0e4-6933-450f-afc9-5b2f907bcea5
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 0ad0c465-fe78-4373-bed0-5f00d4812652
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 2d4647f8-f1d4-4abc-bad9-f4671e981d70
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 277419e4-f9b5-439a-84c5-16b08df57eb4
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 70a6ec23-1d37-453b-801e-6c8380d9164b
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: e0b43cdf-907c-4078-b1de-a279f183be22
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 9b0cdfa8-4b50-45fa-bd40-b71f3ac7e8ce
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: c9ddfb27-bf19-4a14-ba05-ea1a11b70617
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 7ff66a9a-1ee7-422e-93f5-2035808724f9
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 32947055-6581-4c4b-a114-f25d15ca7b93
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: aae057ea-a80e-4c0b-9bcc-eb0d68d9b39b
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: 14833ade-1e70-4bf7-9f59-d8aa6e1e5797
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/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: cbf290ff-0a58-4814-b31c-b0fc1439458c
    creation_time: 2023-01-27T15:24:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/NetBSD_loop.i
    file_hash: b38f47c3dcd7731e15cfc2cee00261f352bac0ed4fe94aeeb81a5c76defb252d
    line: 38
    column: 6
    function: main
  loop_invariant:
    string: glob2_pathlim_off != 0
    type: assertion
    format: C
