- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80eabc70-2cbd-4609-966f-731890a71995
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    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: 2cf36d50-0cba-45de-911b-f2b529683c0f
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    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: f13ad7d1-f09a-4b54-b1f5-3b1ca0ec93e0
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    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: 54dc653e-f960-4a96-89eb-101d0f4e1395
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4c256ba-718a-44e6-a994-f29f4cc47b1e
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d73b817a-8d03-40f3-b009-8619c45f4ac9
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba322f0e-caed-47f3-9008-91a5cea462a2
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0262f31-c386-4775-8e24-2471af3edb7a
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f10c540-3470-46b1-b386-e8695d86c1c4
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec67053d-8ccb-4012-a680-b6590e24c784
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a8aaac0-abe4-4def-bf05-1f9fb031abb5
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13090a52-683e-447c-86fc-76f9992d2d59
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77bcd514-3fe9-48e4-b9e5-df9332f9dbdd
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cdde684-17ca-497d-b8b8-c283c410fe8f
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39577c92-0926-42d2-8f1f-81c695366af2
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b987f39c-d98f-442f-8a21-be95cc7ad52c
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$flush_delayed == (_Bool)0 || z$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0c01eec-17ae-42ab-beb5-6af7c97eea79
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$flush_delayed == (_Bool)0 || z$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ee8a430-d3f7-474d-8471-cf26cb1b643c
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$flush_delayed == (_Bool)0 || z$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d47f47a9-7f5c-4d86-9763-0d5a951e6bad
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fee7d9f-1157-412c-ad9e-b2e415494889
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2f7a266-e347-4b93-b889-dc132ea5881a
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd7cbb7f-33d8-4f8c-83df-aebad1ef4282
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8357be8-285d-4d6b-a914-259a4f982923
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f366f5e-278e-4828-a1b9-d7dba3c8e7a8
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad19246c-9711-460a-8638-1f1f281e5225
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$r_buff1_thd1 == (_Bool)0 || z$r_buff1_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f048cba-f7a3-4e74-8031-d8f033e94f08
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$r_buff1_thd1 == (_Bool)0 || z$r_buff1_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f110a190-d132-4190-8604-06185657dd5a
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$r_buff1_thd1 == (_Bool)0 || z$r_buff1_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cdbf2fa-9469-4733-aee9-4273a92db64b
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 936a950b-0973-4737-a29a-2ca0df40fe8b
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eba2de0e-b6cb-4feb-9f8a-9b864ef64551
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0965234-2b7b-4ca6-9335-c4f94d6875b1
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e1d5f1a-e8d3-4749-b781-80875f7d7f4e
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36851559-4479-4e1d-84b1-e133d6f56cd8
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4909122-0450-4679-80a9-8ec238db99cc
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc81f8ed-9123-4543-89c2-4a123ef58a88
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6a5f96a-3af0-4117-85ee-ea05b3b9de73
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6556495-8ef6-45a8-9d5c-538e69ad3c56
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73c26cce-ee91-43ad-9dec-d95dd7d764ba
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f29b027-1a7f-447d-bc2d-bc7e5a0fd921
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f142ddec-9904-4748-b89e-7c2089cfadc4
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 876fa30d-38c4-42d1-941c-bfd61041568f
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d1f68f0-d074-4319-8570-b40e3c537b64
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 159111e7-3d38-47e7-bd0f-772fbcd00db8
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0_used == (_Bool)0 || z$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6cdbd7d1-06e6-44ed-989f-73dcc2cfccaf
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0_used == (_Bool)0 || z$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f4b25c8-2d00-41a0-a5c3-0d4b66971927
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0_used == (_Bool)0 || z$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cea377e8-d400-4833-b05c-4f4bdc71bf11
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || z$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a6aaaf9-a993-4222-9826-afe1cf78b484
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || z$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fe53114-ae5e-4796-902d-c8a5d9613492
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || z$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db26f2dc-7fa3-468a-952a-123ce74e9376
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fe11aa1-f556-4634-b134-a258fa82b0e4
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4f2fc2e-e529-481c-89cc-7cc74cddfa2a
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a89677d2-db3b-40c3-bcf1-bfff6c908f6b
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24314d53-3b1f-4014-881a-484162024334
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d015052b-236a-4c0d-b4be-d5b6e998b391
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a06deda6-2dd8-4dbd-bf1f-1761ede10397
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2c1894f-0f1b-4353-8bb9-64749a396621
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8888c6b0-c7fd-4159-9841-7962a8ee6a5e
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e95f2a0-400b-4200-9802-ebc1c138adf1
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc507133-dfab-42f1-a068-e7b4f3a980f4
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a5bf09f-95a8-4eab-914d-7c48a5243960
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4173e752-6344-4fd2-bf61-7a161a9a0ad2
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3896bfc-a6b3-4967-9cdb-9730064268c5
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1db8ce5a-6402-408d-aeb9-bd46ae09f113
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b8f0fb9-d011-49b0-8a5a-535c64ed1cf6
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$r_buff0_thd1 == (_Bool)0 || z$r_buff0_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 810789f1-73db-424a-979d-819252806e85
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$r_buff0_thd1 == (_Bool)0 || z$r_buff0_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c6205ba-88c8-4841-adb5-bf223b5e593c
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$r_buff0_thd1 == (_Bool)0 || z$r_buff0_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b228787-8202-48a8-8a1c-a942fcb3943b
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1_used == (_Bool)0 || z$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 915af75b-5169-4151-a2e8-2cd78386ad64
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1_used == (_Bool)0 || z$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa5a74be-f8d9-4266-b866-ed6c7bf6e79f
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1_used == (_Bool)0 || z$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0649fbd-6ebb-4c9a-a939-f96d4efde558
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    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: 3b512709-9d31-4094-94c1-579342a6d0b2
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    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: b9f85d79-c549-4a87-98ea-4257cf59270d
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    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: fdc5fe03-c93a-4bf0-845d-9ad822ebbcc1
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z$mem_tmp && z$mem_tmp <= 2) && z$mem_tmp
      <= 127) && ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99f3bfdb-bef9-4ef5-900a-27a99636b997
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z$mem_tmp && z$mem_tmp <= 2) && z$mem_tmp
      <= 127) && ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43f41367-2b86-4673-bd53-2dbbcada7771
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z$mem_tmp && z$mem_tmp <= 2) && z$mem_tmp
      <= 127) && ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78a716a0-d87a-4ffe-940b-3d348c79ead3
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ebb0af1-d9ef-4160-bd52-f1d1fcb5e07e
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3d4044c-7b60-4326-b4e2-f2c8e6f6e40a
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5678648-1768-4943-9db1-67c7e1209287
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 823
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 601caa40-ec99-4655-9725-e76e861d9536
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 825
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ffc53e6-62cf-45f5-9064-7fd6a12ab123
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9ec25479-4448-483e-839a-d29c4ee3f43e
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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: 8eccd18a-8054-4b7c-aac4-32a0214bfa09
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 793
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6cfe0a89-2680-4b45-8922-8fe9479e7179
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 791
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f9ddda16-d5ce-43da-9a6e-0c1ef1f8be75
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 757
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: de13fceb-4732-43c6-b062-4743ab29952c
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 756
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d6c4d6b7-eaa4-4ce7-934b-67b8a8ac787e
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 776
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 80ba9f76-2223-4655-876f-a165bdef1730
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 784
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 581255e5-b13b-4a18-8b21-2de26725b753
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 828
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6908d1a2-0c07-465b-b02a-6ce73b299ba0
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 830
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 80f28c05-57e4-4a6a-bcb9-5c72062ac98a
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 836
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ab129978-6ef5-4140-a401-e32ddc486ff4
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 794
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 30aa1a22-e7a3-4573-86b9-b6fa0b5e984f
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 771
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 799900c1-51cc-4a0c-99b8-5b1e72e16da7
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 804
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4d10bcf8-aae4-4bdc-80ec-249698289110
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 796
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1d72e50f-f512-44a7-a834-835c575f3863
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 803
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c71185c1-23a3-40ec-8a13-5356c4fc5c57
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 786
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 877824f1-2502-4b32-b78f-9710140140ae
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 826
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed226bfc-f045-4044-b1af-ac873f524525
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 837
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ec323d98-07ad-4121-becf-72253eff6b24
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 766
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9d67b804-6575-446b-aaf8-7bb98f333298
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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: a61b63b4-9d58-4d02-ad66-b46daf73b1db
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 821
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 01b2ff18-d5e6-453d-a329-03e96f7061d5
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 763
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42224c86-3e94-49c8-83fe-b7b5568bda5c
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 806
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fb52a7b6-ffca-4c6c-867c-43f6b1c42d1f
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 852
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ceabedf3-4524-4557-a93f-be8dd3a110d8
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 777
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2e695350-87c1-4d04-8437-106e8eebf1ee
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 764
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 595ebae1-020f-4769-b118-b668b28d2a61
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 783
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4b92bf47-cc7f-48c5-a5ed-9bcd6d9219d5
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 754
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e2efe0c8-f60d-487b-a97b-ce6e438d87cc
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 773
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d6e6917b-6fb6-432e-b062-23bb70f3a20d
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 742
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0b36d6e2-d0e9-41ff-a3bb-84dbd312b9c0
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 753
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 58bb1685-2a52-4c6f-9cea-7c191f4faa2b
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 797
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fb93b681-bab8-46e3-86a9-b55131a88b9e
    creation_time: 2024-04-25T07:37:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
      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/safe008_power.oepc_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: e73cda23545f4a54d3eef0093038f0fb79909f0b7b9d845db14abda8dd1f5281
    line: 774
    column: 3
    function: P1
