- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: befb4f23-54c0-45fb-b326-9a40bef1e0ab
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4c0e423-dcea-4a3e-b6dc-fe7e384199c3
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ca977bc-8202-4399-a0bd-aa85ace438bc
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2702018-f663-4910-9580-31e86c34307b
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    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: d22e167f-5206-444d-a8fc-17c9169fa870
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    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: d40200b9-824a-4b59-b710-32d678e83026
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    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: 079260fc-74f5-4070-8a43-6a3afc65424e
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e98eaf4-360d-4244-bb8d-58d1be5e0990
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04d10523-5579-4b2e-99f2-694243dc3d84
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 388227fa-73d7-4835-89a0-c218e3422a84
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$mem_tmp && b$mem_tmp <= 1) && (b$mem_tmp
      == 0 || b$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d994a867-d72f-460c-bc3f-8df68d9b7f56
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$mem_tmp && b$mem_tmp <= 1) && (b$mem_tmp
      == 0 || b$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 586c0f05-57c0-489b-9ea9-e4b0ce23cd24
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$mem_tmp && b$mem_tmp <= 1) && (b$mem_tmp
      == 0 || b$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1e67c3d-6e4b-4321-8751-f4e07babd6bf
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    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: 6df77ff3-1aed-4c7d-b2f4-b7ca393df77a
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    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: f8009920-c769-473d-80d5-aa1f5f9e72be
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    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: 0ab3f3a5-d42d-4f53-8070-efffb661cf53
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef86e785-17f3-4ca9-9de7-61cfb77530b4
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ae8974c-e104-4d7a-939a-2ad6a54a021d
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7bcbdce-1d8a-4196-9efb-a3f90f53eb0b
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f19029a3-4cf9-4a15-960d-57da3794eabd
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cfd4fee-7470-4751-9167-2c51b8ed43e3
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b53367e-8a23-40b7-9b13-bb3cfe8a770d
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || b$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25c011f0-dda7-4819-8bc1-d74cb6858fdc
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || b$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe9ab0c6-56e3-4a6e-b432-f96d16d6a765
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || b$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c14ace4-d7aa-4232-8412-426135e1f88a
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d20cbd14-5893-43e0-bb21-a42f6cf547f6
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00710ec6-d17d-4a41-98e5-5f481e8e150c
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 336a6dde-6a29-4e25-bd72-8592cb3075b2
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10f6307f-a116-4063-9b78-d2e066224dd3
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 849906c4-b83a-445f-8952-8762424c6a22
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ef6972a-61a5-4102-99e5-01f449d656f3
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1188cbb7-812d-426d-a4bf-bf3dda91864f
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9249586e-fb31-4880-86e5-3864e3eaaf2b
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51cc0127-4815-41fa-ba2b-0173280b1fa8
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c4d6fe3-4c14-43f3-95d3-0fd38ea89fcc
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4e75d69-71b1-4cf4-a8ca-7cd087684fcd
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 312fb7bb-4e2b-4027-8d83-494151f75340
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff1 && b$w_buff1 <= 1) && (b$w_buff1
      == 0 || b$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72640ae4-5949-4004-9a67-8dc6dd4d3fe6
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff1 && b$w_buff1 <= 1) && (b$w_buff1
      == 0 || b$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adb9e85b-b481-40a9-956d-b710b169e095
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff1 && b$w_buff1 <= 1) && (b$w_buff1
      == 0 || b$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b32158c0-6d18-4395-8cc0-e7f19223bbfb
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0418042-06aa-493e-9c9f-9b58165c4cb1
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fc328d6-4803-4477-a556-b3e21453297b
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a5593e7-b0e4-433a-b40e-eb5e5ddbc4a0
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de8950d4-5f3c-4f67-a63f-82734a787409
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fb283ec-01fe-4342-9ae0-821b96c22b59
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ee3189d-6e6c-4eb9-9841-286d4f90815f
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff0 && b$w_buff0 <= 1) && (b$w_buff0
      == 0 || b$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60e31a0f-b331-4f22-b2d1-26032704abe3
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff0 && b$w_buff0 <= 1) && (b$w_buff0
      == 0 || b$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85e059d2-1154-4bf7-81cb-4cd3a7aa2255
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff0 && b$w_buff0 <= 1) && (b$w_buff0
      == 0 || b$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2df6e4e-afdc-4ff0-ae17-72ffeb389b43
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    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: 785a5b29-3ed2-4977-84cd-f37cf0eb68e0
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    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: 1a2bcd40-209c-4a7f-b0c2-e52773a6d891
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    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: d49a63a4-e9c2-49cd-9b0d-08035884bf00
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9322dd2c-2c1e-4474-8409-e50fe67930a2
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f838b773-913e-43f2-a01f-3f4529289948
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4de9b65-3fab-4fc2-b6ee-5e5a62ea70f5
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07f6e075-5c59-4c78-941e-558763b69e49
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bec33a9c-9939-44f5-8261-c4fb1176a9d2
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50759ad4-4d95-44df-8bba-e9cd340ca73b
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41e18c5a-3431-4d23-a5f8-6a37b18f2f3b
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e281d741-e893-4d5a-91a9-b0d30b78cd6c
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fda27829-1d6e-48da-940c-9f26df4ac042
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70207b5c-167d-48dc-8d1e-3f9e91fb51f5
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64e43266-adfd-465c-8fa7-4112ba48aa12
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cf5378e-a1b8-494a-8957-7ae6a06305d7
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5745fa3-72cb-433c-ad54-70772193c1f9
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a1a6144-c182-401a-93d7-f2a40b9b4601
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ce626678-ffd1-4a9b-ac3b-c3637055c528
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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: 680647f6-b9b4-4050-bb78-41cd30b54b64
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 811
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03f43588-2969-48bf-9f99-236f080a0bdc
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 797
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b39c254f-37cf-4c14-95ce-214fb63d834e
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 765
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 350d4dcd-b344-4251-bf61-f65d328a7d43
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 872
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d6a50ad-6601-4ab2-a57d-d932bbb63302
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 764
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 05f17e18-9cf7-44dc-b972-928f3e771fdf
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 784
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 53d05b61-3f15-4216-851c-2c713d440d28
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 807
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 420c0f63-c743-4894-9f82-7dcfddc17b49
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 800
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b83af0e-6a62-496e-adba-080d405139a4
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 863
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0c8ba388-dce4-4cf4-b9c8-57552577b6f0
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 779
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 62dbfd94-26de-4a6e-a2fb-2952aa94353f
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 829
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5acbacd5-5e05-4d6c-845b-87a909cfa671
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 790
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 38cab825-0e9b-437d-8d82-91075ba47f0a
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 787
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f932e0ff-0857-4b11-a30f-cfc1e54d9b20
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 861
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 62c27f9e-a4b0-4c5b-b6f5-dc57e03c11cb
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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: a8b5202d-d4df-42cd-ad9b-51057f364e9c
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 854
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 14def55e-684e-46d1-9d0e-6c7fe3f445ef
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 774
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 12e580e0-6db4-4f51-a8a9-4203363739af
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 808
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9e3fc948-e1da-420e-86f9-3e2616e2b4ca
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 788
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0e68ad03-3805-4031-8d89-616dedfefb8d
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 791
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 41e0e2a2-8931-4220-8663-9193897f1001
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 771
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d64eada2-900c-4105-a8d6-ec4243154481
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 813
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9a3aaa89-8ba1-4962-918d-3e5754093d0b
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 839
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: add7fa7f-0168-46be-b389-691b623d9bdb
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 869
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c0014cd5-5952-4129-9064-e1a925a3e497
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 870
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3661e668-29ea-44f6-a4bd-6487c8c51240
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 837
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 514f3bc9-97da-4b80-9abe-3ed708d86bfd
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 785
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7cf2257c-d046-49a2-8373-63201baba164
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 814
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f9b79962-f122-436f-96c1-6c82265fd3b2
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 810
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 44aa0781-9500-40f4-a950-f9d891f78c52
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 772
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d63d5955-d381-4a78-a328-a3007b730260
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 836
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0afeb6aa-b473-4ba6-8fe4-f01ae36e3f90
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 762
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a327f5a1-7b7f-42cd-b4b1-b2734d2d73e6
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 830
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d2668bbe-b221-4283-8141-1cc9d4087e8d
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 781
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1a0469f8-ea63-47f6-ae3a-b7e939fc46e0
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 245211d9-ab17-4903-8fb1-d8d2f307c9e1
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 761
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 706c3ea5-62f6-4b9d-a8e5-4e3b787c0ac1
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 805
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: abebc8a1-b342-4b7a-9596-4f1acad2b08c
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 798
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bb269002-2281-40ad-a8a3-9d9001dd759a
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 782
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: adc8d6b6-2349-4fdd-8e1f-ce083fdbd661
    creation_time: 2024-04-29T11:00:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix033_power.oepc_pso.oepc_rmo.oepc.i: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
      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/mix033_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 7ebc335b60b8cdd623e40ee7c2c99e8e082656d42f1fdf6911dd5259073d8a45
    line: 859
    column: 3
    function: main
