- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f676debb-ea72-4c03-9bc5-7a58eda34bd6
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 157
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_5 == (_Bool)0 || is_null_5 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12c528cf-0b32-41b8-86d0-98c6f731363d
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 158
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_5 == (_Bool)0 || is_null_5 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: beb7bba7-4bbb-45b9-97f7-a87f297ce320
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 159
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_5 == (_Bool)0 || is_null_5 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78398fe7-f8dd-4db2-854e-f12d43914e8f
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 157
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_14 == (_Bool)0 || break_14 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18e9f5f7-6b80-462a-9058-0573c0830409
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 158
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_14 == (_Bool)0 || break_14 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef70f747-906c-4690-907d-db00b5cb68f1
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 159
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_14 == (_Bool)0 || break_14 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 602d40ca-6a58-4d39-8701-eb0177db8cc7
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 157
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_1 == (_Bool)0 || is_null_1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c853703-a6a2-4e5e-8246-6bd34de8a19e
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 158
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_1 == (_Bool)0 || is_null_1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2881dbd-653b-4b21-a91f-fa9eaf4a039d
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 159
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_1 == (_Bool)0 || is_null_1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d3e8f25-82e9-47eb-b01b-e8c262929e6e
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 157
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_9 == (_Bool)0 || is_null_9 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07ef4626-5e96-46c0-a03f-19a4c3d5107e
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 158
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_9 == (_Bool)0 || is_null_9 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f77f7794-5b6a-4a55-a155-e7e36a7f418b
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 159
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (is_null_9 == (_Bool)0 || is_null_9 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7db64427-3972-4685-833b-f1fff81c37b4
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 157
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_17 == (_Bool)0 || break_17 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 377fe7e1-d0f2-4eb5-a69d-4bdb6fe7d16e
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 158
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_17 == (_Bool)0 || break_17 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09d870a3-81fb-486d-81b4-2c5c628be33e
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 159
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_17 == (_Bool)0 || break_17 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0686f211-aa0f-4447-b7da-ee4bdc6be06b
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 157
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_20 == (_Bool)0 || break_20 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97df884b-7fb3-48be-b7db-71dbf4e404b5
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 158
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_20 == (_Bool)0 || break_20 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82ab91cb-eacf-4dce-b25c-5557ccc26332
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 159
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_20 == (_Bool)0 || break_20 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 71103181-5ce7-4c86-b87f-dd5b89d9a897
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: de3c40d7-e422-4f16-88f0-ec494d96f20c
    creation_time: 2024-04-25T07:42:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-subst.wvr.c
    file_hash: 47976145f2a7f206dd7d2e7a0ffeac879f94f33f7a5b87161ebd997173567eb0
    line: 156
    column: 3
    function: main
