- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9209fecf-0cfc-457c-8cc4-1d859b8a4375
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 145
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4aedf769-cb0b-4b24-acf0-eca8e2c486e8
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 146
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecef2e3b-effa-4c59-ad0e-a2171b17c732
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 147
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd90a8ff-674b-4c57-82fb-830c45de1da7
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 148
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0100396f-a507-4d41-a2ca-baa52b72eb26
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 145
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30a2bb82-bde4-4eee-ad89-e6e642db026d
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 146
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60ae8567-4bac-4dda-b239-4ea3e3d0d852
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 147
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffdc93f1-9e21-49c2-800c-58072eabfac3
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 148
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfc85570-25a7-46a8-914d-804e2e5d8640
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 145
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (0 <= i && 0 <= j))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 619ded90-abf3-4114-8fc0-2a03ba84af0b
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 146
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (0 <= i && 0 <= j))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b33cf8cf-9098-4a2b-8511-c4d4c0203242
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 147
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (0 <= i && 0 <= j))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86307cfd-aeb7-4efc-9b81-026f257142b8
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 148
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (0 <= i && 0 <= j))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 4f5a53c4-7991-4799-aa3b-99861c132dcc
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c5422e24-cc8e-4b40-96ad-c3d9276fd260
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 61
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9840b8c2-42f5-4fe0-a475-aec4eb9cece0
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 75
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a0f00bff-7b28-46c0-a1e8-05a565d34078
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 92
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: db947e30-68d5-4dc4-8d19-0f8cdb207768
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 114
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2812b75a-d150-42eb-b553-b9b436cff52d
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 52
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3988cf7f-6a9d-4a8b-80b7-c15b0519df31
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 55
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a35878a-c51f-4f0a-8789-00a3ac6df5b0
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 72
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 344cb255-0c94-4e1d-baec-cf05a858ab64
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 117
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8ca15073-8144-481c-92f1-86312106dce5
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 96
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a5c8a205-3609-4f4f-9cb6-ebe663b0124b
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 58
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 25cd31e8-a8f1-407f-9588-73412cc079b4
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 79
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dcbfedbc-093e-427c-80ac-39e79254861f
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 81
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4529bb91-5ad9-437f-a5ee-367c6a26c5e4
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 115
    column: 5
    function: thread4
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: bcec943c-403c-42f5-a757-9eaa928773f1
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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: 96fe654c-b287-4c84-819f-42693995397e
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      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/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 144
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f44b097b-66c4-4447-9043-e8caa570dcdc
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 68
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 85470bd7-6cc5-4971-bd2c-dba505b2136a
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 78
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a13957b4-638b-4119-9379-40f8df5dabaa
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 59
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8eefa2e9-f567-474f-ae21-7296f29c74f1
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 76
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c05c4be6-c3fb-40ef-8ec9-18f5a69f0a81
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 99
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42705b1f-e25e-42c2-a9fd-f0abf92c4845
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 90
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9eec9d4b-a2b3-4519-b546-d626a5785741
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 88
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fe7820d2-5dbf-4527-a017-2ceb7ea35f4d
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 56
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b1c2a7a-ccb2-4c40-8c54-a5bcaf77dac9
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 50
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a561f4a2-fc0f-4efc-90ac-1553cd9f6cd3
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 108
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2fa4c549-7b4b-4855-a9c3-8af22ccc24ca
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 110
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d0b6a102-1417-41b6-8075-823139801450
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 106
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 68341384-e1c8-4f26-89c1-642b392a1251
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 70
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4ab3bdb6-84f5-4991-9675-13f14d7b5635
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 97
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0fd2c17-13c5-41c6-beba-881a34bcc6f7
    creation_time: 2024-04-26T10:51:17Z
    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/popl20-bad-buffer-mult-alt.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-buffer-mult-alt.wvr.c
    file_hash: 2e9e4bd6e9b16aa5f22ad2335ca34ba741869a12ab5a04a80108cf42ed170c0f
    line: 48
    column: 3
    function: thread1
