- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b21a9b4b-b83e-4910-b899-6fc79e3092b3
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0933f36c-57b0-42c6-992c-ce52ce9ee2b0
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78b03d03-88e2-47c4-a589-6ad58947d566
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0eb0e2bc-e0f3-4789-936a-bfdc0231b0c7
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    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: b92cdad2-75d8-4696-b8d0-452d59f91d2e
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    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: 570c4894-6ec0-462a-b22d-ea21e2575853
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    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: 3b2a3e81-2ea2-491a-9968-bbb79dbac802
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ceba988-0d46-4dae-9431-59adbe71e76a
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 985483f1-3daa-4981-8a69-3402f497407e
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d97ffa9d-4908-402e-b852-7dd8ddfa3c9f
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16d3bfc2-362a-492f-b4ab-61b17daffe09
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db4806b6-c486-40a0-9f07-30edcb1abe95
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 608654b8-81ee-464b-935b-7073365a994e
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38b332ac-738c-455e-b297-b079bba07b25
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 041bde4f-3577-4871-bda8-69586c65b0bb
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efaa749a-f5d2-4227-981a-4e5aab76db0b
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    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: 90ab2d9d-4180-4df5-8c63-146a8db9f5d0
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    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: 37342b78-77a8-4fcc-8a2c-425ca5eac8ce
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    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: 5081f1ee-939a-485c-bbb3-47fc19e271a1
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31a3041d-f1dc-4230-8fdd-c06a8b48cb39
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47a5d991-64e6-4a81-9087-f44186647b0b
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd8e45bd-e19e-4bcf-87a0-34e697fd4bb5
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    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: ab546c3e-70b4-464c-bc49-b0e52f2f1e23
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    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: 725765e2-b519-4aba-a3d2-1837639ceef3
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    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: ec8142fe-f47d-4735-bb2b-4bcd6ee85f3f
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7abc3374-d87b-408c-a099-467849262747
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1e4afda-9aac-4fbc-937e-34c5326b1d92
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0eb77850-d0c5-4eb0-b745-b34d2eeee568
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71e98e2a-cc14-4507-809d-f692ee9abefe
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 66a4f25c-ebff-4823-8569-61b4ecfa9704
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b9770f8-721f-4f35-87d2-3ea2b6939da8
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8e49a06-211a-49fd-815f-70d21fabec54
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dcd51359-c64e-44a6-b63b-e1b816320be8
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6e63633-272d-4ca2-ab19-769675e24e51
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    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: 5fc07358-9fa8-48d5-989e-2d3100937ae2
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    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: a080814b-9970-4784-9416-4bebd749f52b
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    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: fcc02597-6fec-4594-9f0c-66951b65d5fd
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 528dd375-7f47-4abb-8c9f-4ec092dbe4b1
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 080cea23-a6d9-4904-ac0c-02fb69cf987f
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79d15d06-b34b-493a-9dc4-232d08114174
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bff5e1af-ab73-4379-8e08-0a788b28ca04
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3797787-f3a0-4581-ae6b-af2bcdde8780
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a105716-e23f-4594-97cf-5c592c118070
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96d37595-5322-4f32-81bb-2877b680df7a
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b898ac45-3317-41da-95bf-4f8d81e454bb
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea3fb4d5-7006-40df-9151-7966c4b6a7ea
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4f4a217-8f52-463d-87c2-be5ce0535bb7
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcc5aa50-e963-4b22-a500-070f8714faca
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de0d410a-909e-42d3-a181-8e5b62383cde
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 927cc0cd-794f-49a7-ab5f-241a25f80836
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 494c08d2-4bf8-4b79-aef7-3afcc760e2f5
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 04b1a0a0-eb27-4053-be79-105bdda12cc9
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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: 48648f69-e843-45ad-b5fa-01618f9dea60
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 745
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7b9eb668-6163-4d3c-934b-c750380f1fdd
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 786
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 04767516-bd0e-4fa9-9d9d-71e3bbf1a4b2
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 829
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d28ee695-4df3-4e99-9ae8-4ac98116545a
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 758
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2174ab3c-1806-4c1a-88c1-874a70bf6b6e
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 797
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 979157b4-619d-4362-8d36-1f007b131885
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 790
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 825cc2af-36d1-427b-9106-b43315634d79
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 755
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a781d2fa-2383-45c6-8a51-a54ea290b050
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 757
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fbc1b79c-d14a-4181-9b0f-840a90839b0f
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 789
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4c292876-b49c-4e3c-9f60-4aa621aded1f
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 821
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c321c781-44fe-4d4a-b0cb-955953a58079
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 748
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 3de2cd25-46e3-43da-991c-1986dbb031e8
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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: 15cb804f-95a4-4673-a20c-40d84c089b4a
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 814
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6890f782-f98d-4f99-8357-3e33c2d2e919
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 819
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: abb49e36-08c1-4fe8-97a4-9b762e9a9007
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 760
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fafb4593-2f7c-4c24-b951-dc08c94b74e4
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7623ba74-a192-4da6-868a-7b2e6b9f8792
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 746
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5846a5df-fa81-430c-b825-da76804ca216
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 845
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3357a780-462b-408b-829a-2b242277defe
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 787
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 919271e7-34ea-4a46-8004-d330bef96bcf
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 823
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7ae87428-fabd-428d-9250-e904d2768b6b
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 775
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 796b17b4-77a0-4e5b-a3f1-5a2027883113
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 770
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2fe235cd-7844-43a6-8111-b05bbab83b6b
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 742
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4790a241-b970-4149-b8ba-16f7f25864c9
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 743
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0fb3ce2-d876-45df-94ef-d74a5e5daecd
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 830
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d746f815-2647-4cda-ba03-b3cd1c10e577
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 747
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6a343e83-92bd-4d4b-88db-48a443bbdd79
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 740
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 72aa1002-1232-481b-b7d1-5140d3aeb15d
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 761
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 99c869f2-8844-4b0f-aa8f-32510f6e993e
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 767
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b039919d-8d7b-4b4e-a52f-047e1f98dfcb
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 768
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1afde8ce-010e-4f96-bd2c-fa7387261886
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 799
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 30757892-d843-4488-821b-7a22ca945486
    creation_time: 2024-04-30T09:36:39Z
    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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
      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/mix056_power.opt_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 0a03a5fc32da65217c1f578a6fea0c2c0e07a09fd6b8159429f8d1aa4c1c45a8
    line: 796
    column: 3
    function: P2
