- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddbf40d9-1a5e-4b39-8c91-269543537459
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    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: c0d09cd5-e6ef-40f5-85f9-0bc8c9bdfbce
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 783
    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: 978a554d-4d6a-4c37-a67e-881dbfd8e76d
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 784
    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: aeffa262-1ed9-4deb-a375-22edaa380404
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 2) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f57f9fa-a09a-44e0-9624-1b34efa22cd5
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 783
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 2) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58bb1ec7-9d3d-4e8a-8db5-13c0c56be688
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 784
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 2) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9754a4f-d053-4ebe-adc0-8a0215e0c24d
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d98a3f43-7f06-409a-8df7-791a0600e1b0
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 783
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53bd4dc8-fe77-4e14-975a-d5cc7f0e7e64
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 784
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e89b7d6-bfab-463e-84b5-34aa1b916bb3
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p2_EAX) && 0 <= x) && 0 <=
      y) && __unbuffered_p0_EAX <= 2) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 2) && x <= 0) && x <= 2) && y <= 2) && y <= 127) && ((__unbuffered_p0_EAX
      == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX
      == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0
      || x == 1) || x == 2)) && ((y == 0 || y == 1) || y == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27b52df1-fde1-4ea6-bc43-eb44896bbde4
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 783
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p2_EAX) && 0 <= x) && 0 <=
      y) && __unbuffered_p0_EAX <= 2) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 2) && x <= 0) && x <= 2) && y <= 2) && y <= 127) && ((__unbuffered_p0_EAX
      == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX
      == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0
      || x == 1) || x == 2)) && ((y == 0 || y == 1) || y == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0295f724-d67c-4906-8a2f-6417f9663b1f
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 784
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p2_EAX) && 0 <= x) && 0 <=
      y) && __unbuffered_p0_EAX <= 2) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 2) && x <= 0) && x <= 2) && y <= 2) && y <= 127) && ((__unbuffered_p0_EAX
      == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX
      == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0
      || x == 1) || x == 2)) && ((y == 0 || y == 1) || y == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4596cbe-5c3a-4e46-a3ca-5f7f8a48f5e3
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 781
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56d8892c-d8a9-4e67-96fd-8eaab6520574
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 783
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94b0abc7-db26-49c2-9174-9a10050ee083
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 784
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8bbbc1e-2a52-41c1-9ce4-c676a4d7d5f0
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    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: ca6ecbff-526b-4b7d-9bb3-f56a09573212
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 783
    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: ac5aa942-654b-44cc-a796-071b4444f446
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 784
    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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: fba9a60f-d972-4e5a-9b54-b457d05f753b
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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: 3ba1c135-d701-444b-8632-7f2e7d9d171b
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 749
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1139bb9e-b99e-40d6-be6d-3d146e322689
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 760
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d56ba765-b7e3-4699-a72f-ab4b21501028
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 792
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f6ebfc06-7de8-45ff-854b-9c58378d2901
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 761
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 402786fb-8b26-400e-9c6d-943e77944680
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 762
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 89d264d5-441a-4dbc-920b-98e3ff0ab85c
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 742
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8c411267-5c54-4c13-a30e-4476dcc7d0ef
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 757
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3a07b349-6cce-4b13-850e-f69619f1c29f
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 732
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b8121dbb-54b5-4e36-821b-1cd6169f6044
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 726
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fefcefd1-6899-43a6-9ab1-72794377c05d
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 788
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 83a2496d-f23d-4b48-b948-1e23d409fa0c
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 727
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3eb74524-0944-4234-9d09-85d86ebb133d
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 756
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 168fb062-8d61-490a-9ffe-5deb74c32802
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 754
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a12fd3d3-3d0d-4f12-af0d-749a45be23c2
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 764
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9ea2df94-fda7-428e-8f4b-0705f5e1c5c3
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 747
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dff27228-55bd-4bcc-b88a-67860ab789b8
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 724
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 941e6379-6002-46d7-9ae4-68cc27b5859f
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 744
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ede423a9-47d2-41df-9451-4e736a92abd0
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 725
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a0e1b442-760f-4248-8b29-c0c4a15eb0b6
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 729
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a943e69e-e5cf-4b8f-afac-4dc6a263d386
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 746
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fc3463a2-d3b7-495b-8c9e-3780e96b18e7
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 784
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7e3e29e0-38e1-4f1d-9542-caabd1ccc1c5
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 722
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e7e3fd6b-6c30-4bf1-8eb5-c15a6754aa9d
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 786
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ca6b02bc-89b1-40c1-8dc8-11dedee3fe95
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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: abd1c274-fc70-4080-bec0-a9116a605b83
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 779
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 626cfff6-2061-4436-b99d-817b53432b3c
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 741
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f6f257d7-5ac1-46cb-96e0-81437b95fce5
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 790
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7f5954df-79b6-42c0-a54e-e6c4b75236ee
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 734
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3183d111-b556-4b4d-b7e8-015d29d76004
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 759
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b47e36b2-7c09-4f9e-b323-d399bf653711
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 745
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: af8e4a7c-935d-4156-b84b-6ad842bad965
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 789
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4fc33703-3e67-4750-87aa-fb6b5206583c
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 731
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 51da9c16-bef0-48d1-bba4-f2e9d5508385
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 739
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 75f77b50-9039-416f-b60f-3179eeeac2fc
    creation_time: 2024-04-30T10:01:17Z
    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/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
      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/safe015_pso.oepc_pso.opt_tso.oepc_tso.opt.i
    file_hash: 5350e4ca2594121b974c795f0a5f8bd0219ad1e56ba65ceaff14b5f6479d7178
    line: 730
    column: 3
    function: P0
