- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c232876-2c37-44d1-8c53-b68c45860950
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 778
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35d158b6-9fb0-498d-87d0-2cafa65270bf
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 780
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b824ee5-b0ea-4f70-849f-45ef3658d1b7
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2eb785a-01eb-4804-a531-0fd51d861087
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 778
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dabd2808-909b-45d4-8205-d6173abc2a81
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 780
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05776d6a-f915-4cbb-abaa-11c2899bdf6a
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7791155c-d70d-4f72-a6dc-e1f721441b32
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 778
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01622347-0779-4e7c-a78d-4913f6186d75
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 780
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be9edf47-393d-4c32-add1-fa31f59b97bc
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0959e30-2f23-487f-b89f-7cfdf19f0957
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 778
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6caff5db-8542-4e49-a8af-36bf931aba01
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 780
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38a4c871-a3a4-4d41-b84d-cc4af097cad9
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 093c2121-31c6-43ea-b6a7-3a1c833463e1
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 778
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67b47feb-120e-42b9-b2a6-be7bc4a1dcad
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 780
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c619b04-a0ca-455d-a16a-4cfcee80487c
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 647ad8d2-253a-4505-9a35-f97fd9383373
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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: 1ace87e8-a80b-4689-a930-542239d297fe
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 751
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e23bb859-439a-4c90-9bbe-0f079e538ef8
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 785
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ab431698-90be-4167-be3f-474b5cec1146
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 789
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5a170999-712c-4045-aef6-d7db20ecf912
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 761
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d0d648c4-4ec6-4ef9-afe9-580883b1e14b
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 758
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6dfb2983-6950-41a0-8cc5-b7d218806ecf
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 742
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5c6eccef-92df-4d69-84f1-b27a65e85343
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 757
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a9d0b19c-c405-44d3-be32-cff885b3f003
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 732
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ff43c78e-fb44-46b4-9e3e-c1708ecb09f4
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 726
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1502fbb6-32e7-4a55-b1b6-f035f46d0ab6
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 727
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 495504d5-f03c-42ac-ae1c-0fc20559409e
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 756
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 132d48b5-1804-4b69-922c-b4064d04b555
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 753
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3e70c911-8099-4ca0-92b5-11ee7755b2ef
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 754
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0b9d118c-3fb5-486a-9c50-0f09d104b31e
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 724
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 946a58c4-b297-46ad-b5e3-18f97d0f516e
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 744
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 24af0e08-0eaf-44ee-8ce7-90b6bbed6885
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 725
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 60090c32-9643-4c93-b0ef-1dc4c861ca54
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 787
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d2ce0e41-e46d-4feb-b429-9a0b1416db12
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 729
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 326d62c6-8d12-4f9e-89de-63b4d53bbdc5
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 746
    column: 3
    function: P1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 732297a8-8439-46fc-8cc7-d782cc171bf5
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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: 596e0554-047e-49fb-b7cd-36032e523335
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 776
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ddebb3b6-63ba-4f2c-9914-7437950a5efa
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 722
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1ba074b2-e42a-4840-a689-250eb571d261
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 786
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f940523b-691a-45b3-962b-a4e2522e22c2
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 741
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a7d11da0-c30a-4f62-b8ae-771dbccf4df0
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 781
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cb4f78ce-24ae-4bac-85ac-02c6553d11aa
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 743
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9ae0be9e-3fb0-43c6-ae47-48f1d0d91346
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 783
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 157a840e-be44-4461-aa83-f2d3b42266e9
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 734
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f9b506e-0853-47ee-9298-057e3d3c1a77
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 759
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fdc9a027-84ac-4022-8c68-a8463a8cf388
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 731
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8c5480f0-c9c5-4324-8489-cfcf1816d780
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 739
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 59c789c2-6ea7-40f5-b88e-64333baf6203
    creation_time: 2024-04-30T10:58:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
      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/pthread-wmm/safe020_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 8e0b8e6efb6fc18f3ca2ba094d3acbfc6a07fbc0100e70485e3a3a84ea56105b
    line: 730
    column: 3
    function: P0
