- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 406ff37a-63ad-4204-a323-4b9229f1888b
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 123
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_13 == (_Bool)0 || break_13 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 91fc45cb-7033-4148-ab56-096d74e3ab7c
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 124
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_13 == (_Bool)0 || break_13 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e4b784a-ffd2-4760-b997-c5525c760631
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 123
    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: 745233dc-8c3e-46ca-9054-5e9c81d5b52c
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 124
    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: df842281-bfa4-4536-9a21-9ca22edb3ad0
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 123
    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: f7ec3a67-1630-40c9-8ff8-5a7ddece4722
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 124
    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: 42e8465b-4118-4393-9d8a-8504665b6a1c
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 123
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_10 == (_Bool)0 || break_10 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a733cb9-2974-40ce-b748-d9cb4797b3a5
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 124
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (break_10 == (_Bool)0 || break_10 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e0c34c6a-3a41-4273-b1bf-9c9a084734c6
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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: 24e92262-5c31-45d0-90e7-e2a6d368ee8d
    creation_time: 2024-04-26T10:50:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-nzb-file-symm.wvr.c: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
      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-symm.wvr.c
    file_hash: 48ddce9ee02b3ea4431cf137593b71facb450c3e223dbff4f116c3c0ac1377b5
    line: 122
    column: 3
    function: main
