- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9e487ca-1828-4cb1-b29f-b8999fb6328d
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state
      <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state ==
      2) || manager_state == 3) || manager_state == 4) || manager_state == 5))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a4a973d-c802-4b7a-bdf9-c33b0f6202ca
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state
      <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state ==
      2) || manager_state == 3) || manager_state == 4) || manager_state == 5))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a071dcf-541e-402e-9f5a-c9ca2f04215e
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state
      <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state ==
      2) || manager_state == 3) || manager_state == 4) || manager_state == 5))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40b9213f-211c-4763-a97d-4f5063b0052d
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state
      <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state ==
      2) || manager_state == 3) || manager_state == 4) || manager_state == 5))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97668880-cdbd-46e6-9e8f-71516955103c
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state
      && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ffbf902-7ada-4771-a1cc-3f26ba094b6c
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state
      && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00d9b73b-cffd-4225-8046-7b42988db9ab
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state
      && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd007790-662a-476c-96c7-a296fdc54e12
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state
      && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df98a95a-bc79-4bd8-b3df-ae842765490d
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state
      == 0 || node2_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d58a03c5-e38c-498f-a715-e5d849698ce3
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state
      == 0 || node2_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3643cf8-a3a1-4c9b-96a1-77ca313c69bf
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state
      == 0 || node2_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b72003f3-1322-42aa-aa19-93036cf64947
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state
      == 0 || node2_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7b6a228-a1ba-459f-b0c8-c14755dd4662
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state
      == 0 || node1_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14b3328c-5595-42b1-96c0-f335f7a6b75b
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state
      == 0 || node1_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97cb060b-bac5-43d1-b439-c929435f8b54
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state
      == 0 || node1_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc73e260-58c1-49ae-9773-fedf7e3ae385
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state
      == 0 || node1_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99de33fc-de16-4959-9d70-e1cf5b81149e
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state
      == 0 || client_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e98ead9-ef00-4718-a25a-9d08b220a317
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state
      == 0 || client_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed478942-1dcd-468f-8c68-5d2dc6878e67
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state
      == 0 || client_state == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ffb2a73-6fac-404d-a635-443ae8588e04
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state
      == 0 || client_state == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8be68570-af93-4fa7-9bcf-aa948332b726
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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: 76b978c2-1784-47f0-b0f9-387ca53a513e
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 116
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b454eaa0-39a5-4760-b7b8-c276af7a4d14
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 82
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1233c931-b5f0-473e-b5a9-757f78a3d53c
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 109
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4305cd6e-988f-4b19-8588-65c255ba8d43
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 61
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0ceb1c05-72b7-4029-84a2-029c7e4a0317
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 73
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6b089091-e25c-4cdb-a384-9bbf2ca8299f
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 153
    column: 7
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 29b0fec0-f722-4110-af91-398c643ddff8
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 75
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cebe22a0-883b-4be7-9e4f-780802076ca0
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 87
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9edce86a-47d7-4c9f-8305-ef4dd3804436
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 80
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5e63aaa7-46e7-4353-a044-16ee3b04b858
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 89
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aace3902-f90d-4689-be5b-9eee15925766
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 155
    column: 7
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42f9bcbe-6c50-4449-9d80-5729cebbf25f
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 54
    column: 7
    function: thread1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 68e6bd52-9c2c-4dbe-b01f-d7c57c0a7e87
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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: 40a4bbd5-73a7-499c-a495-925540841afb
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 196
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 105db141-93f7-4a45-9ddc-6ed2a6a4e818
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 133
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 626bf388-aedf-4b7f-8926-a72763887253
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 131
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c1162fa4-8914-4f8c-b6dc-5030ec774291
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 111
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 11ed6f0d-d899-41ab-8f08-7c42dbad26d1
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 66
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1f9b6db7-0d4e-4d91-9877-fe4ebc74ed75
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 160
    column: 7
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ad24d792-7d99-4895-85ea-82430fc8ab01
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 68
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e9de94d4-5ecc-4339-b7b7-8c99c3bb8a0f
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 94
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cd8304c0-cd81-4fde-9a54-281ceaaa38cf
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 126
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a819417e-9428-42a6-ab6b-fcd46a74ab3c
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 138
    column: 7
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: db4c6e2b-e61b-4e2c-bd34-6d3607f90993
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 104
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 98e9b6e5-112b-4329-bc41-313ff54a051b
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 148
    column: 7
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d8e253b-b0bd-4da2-ab8d-bf8610fe9469
    creation_time: 2024-04-30T09:43:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 59
    column: 7
    function: thread1
