- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a86997dd-e9bf-468a-b8b2-3d77f99b6ec9
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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 <= client_state
      && 0 <= node1_state) && 0 <= node2_state) && client_state <= 1) && node1_state
      <= 1) && node2_state <= 1) && (client_state == 0 || client_state == 1)) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: 11505ff4-7c8a-422c-aece-6b11ca3f8be3
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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 <= client_state
      && 0 <= node1_state) && 0 <= node2_state) && client_state <= 1) && node1_state
      <= 1) && node2_state <= 1) && (client_state == 0 || client_state == 1)) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: f21c4edb-46eb-4507-9b1f-987187bc6500
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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 <= client_state
      && 0 <= node1_state) && 0 <= node2_state) && client_state <= 1) && node1_state
      <= 1) && node2_state <= 1) && (client_state == 0 || client_state == 1)) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: 08fa0a44-de9f-41c4-b316-107247e21a73
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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 <= client_state
      && 0 <= node1_state) && 0 <= node2_state) && client_state <= 1) && node1_state
      <= 1) && node2_state <= 1) && (client_state == 0 || client_state == 1)) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: 6e1e454b-4840-4ebb-a3f3-0e7da2f08365
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 2e242925-0dc6-4636-a2f2-a81e90c1c7a5
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 8bd03947-d2af-4dff-bfeb-82ac87519166
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 6250f92a-a83a-41ce-8d11-a53fcafdd461
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 18ddf89d-95c6-4061-8c6d-ddb0979ebe82
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 060834b0-4481-4b1e-83bc-25cd17824c46
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: e31cf7ec-ff70-4bb2-8bca-468a8ba2f693
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 23cf45f4-0de9-40bb-8fbf-039eeb449059
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: d7f59188-4dc4-4882-aca0-1b16b6c2366b
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 8383a523-97e4-4334-bcc7-d2349961aaca
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: e65b4374-bb98-4a7a-b3ac-d6c2b4bfc50a
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 22a1b25a-5074-4b5a-ae38-908c5e165c7d
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f6a3d11-2abd-4813-8ef2-19be5a085331
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 7664697c-a1f5-47d4-90f9-6b6347552d52
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: fca9fe11-9ecc-4050-b65f-69a96a19f217
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 42480c20-196c-4f8a-a004-c2ea5e71e81b
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b2d2a49b-a0c4-4193-9d77-be4bc4580ffb
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: c027271b-a123-4511-a61b-bbf2c33278f2
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 2b276712-b22d-4310-9442-11e7af2e93b2
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: d7733ebb-03a5-4f83-b3c5-4265b981bd69
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 706511d5-51e4-472f-a393-3db775c344f5
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 3e5e0c3c-c533-435d-a911-97b7ac2ae3c7
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: fc072f6a-1403-4558-ad7b-63e0899b79b4
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 2e8effec-dd37-429b-bf3b-a5e5709c112a
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 8a053d5f-9fef-4a61-a02a-d3c00962f7e1
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 5dd11b06-2b48-4b52-b5ed-5780513861cb
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: a21fca3e-7c6b-4c44-8050-cabd6cbbaaa0
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 9edef390-f4ea-4737-8be5-948feee3181e
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 57bf7a84-2fc1-4123-8869-1c3c8adf371a
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 935924e0-f79e-41d6-be1e-5259627fc9dd
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 91aefe9a-28a7-4e3e-93ac-e881728b7b50
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: d6255351-dd0d-4335-97a9-db64e4bb5e1c
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 1d664636-90a1-41d6-b542-1b1c8990a75c
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: b9a840e7-75be-4150-a857-8bbbe7670798
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 5fa9ebb5-8d13-4a38-bf9c-17f266f1e247
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: a6f20098-50c3-40cc-953b-b5da7a24c208
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: da99344c-17b2-4943-b288-46b98b93e2ad
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 7c432426-92bc-4efd-817a-790eb4490f15
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: aa8f42a3-f1be-41e2-983d-c6ac0182acd1
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: b8e94dfe-ecd2-4d31-af6e-e0998f4ec9e8
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 9edc5c8c-bab3-42a7-bfdb-0e6064f41f91
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 665b38dc-3445-4324-ace9-ead682609fcb
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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: 81911517-ab5f-4ed4-a234-427a5ca7a136
    creation_time: 2024-04-30T10:08:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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-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
