- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb47eea3-64a9-4b01-9dbf-604f39532c25
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a7da383-0ab2-478c-a82f-afcebb65b849
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72211cd3-e5d1-432e-b964-d667477407ff
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25c973a6-b33a-48a8-bc9f-a81ccf9ac8b8
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f35f084c-9ec1-4636-95a3-afa370da5844
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    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: 7791eeb9-898d-4f4e-baca-aae578b744bb
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    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: e3672568-dae6-446e-873f-5ba3ad6e319f
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de6874fa-338d-431a-b762-0e9994323963
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d94a414-72b2-44c5-bcfb-8a73f66d7ff4
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d71d3014-f0d4-4a6d-b1e6-aac6a8c981bd
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad3455a9-b3b1-4f7c-9e9b-f81a070e50fd
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b8c372d-f697-4cc8-bc48-eea803fe249e
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56380d6b-72d7-4700-9d0a-962ffbc057f7
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97c010b8-4e46-472c-9d98-6394a9829b93
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 782c12bf-47df-42ca-b111-5bd8ca2549af
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6654011e-bcf1-4950-b093-842a578507ed
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    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: f04ee863-bee2-4cfc-aa7d-5c6014b076c2
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    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: 4b65678d-661e-4a9a-a335-f377f65cdda2
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    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: f306ae41-6c9a-456c-bed4-e5829ec8675e
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f8be1a5-32c3-4593-b34a-d1a38ed1029e
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61b19b91-1ce7-4234-842e-8aa0ba247388
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ece37024-08b3-4b91-9857-ea639a927854
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    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: 20794a13-4580-4239-b907-d1b6815a91b2
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    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: cdfa84b3-d73e-449b-9770-b4d630b4c5ed
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    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: 6c630396-55f4-4563-8204-fef87d681d32
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb8a7125-d3c0-4f77-9744-1e6915f7ee3d
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62f27c63-6d8d-4ed9-83af-6b71850fada7
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55d70769-a253-4f0d-a686-0f026c9ada5c
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5b92eb0-df68-449e-a67a-73b6fd2d8124
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85b99720-671f-4b26-b3ac-24230f7d488f
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26797b23-96c6-4420-b9a0-c51493cf001c
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90e3cf63-a758-455b-b401-4b20ff42e49d
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb215e9b-fa2f-4c00-b7c5-773b4afeded9
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da208267-1c88-498e-99a9-24be076a991e
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9578f7e-916d-4b40-ac50-1d71ab277ceb
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4875019-0f8c-4282-ae6b-1d062a8d3941
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 221a8558-4c3c-449f-9bda-e48eb5bc0fd1
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 720e61fc-505d-493b-b857-c4c3865ad9a6
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32751e51-c4b1-4cb9-8280-3f1f311214a7
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc930594-00eb-46f4-9f96-fb3fa7525d2c
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24d81bde-beae-46bd-be3d-92755f9ac33a
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0644305-1e17-4155-9caf-5182feec0846
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c624819b-c1dd-4c99-884d-87d4d9278253
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcf21a07-0991-4117-9016-d574a1c29360
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4c7fcad-91a6-41d3-856d-d65d88a9bc4f
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0fe9737-2573-40ea-8350-085d4223b692
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47b4072c-e7a7-4873-a42a-ccd4671fada0
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec54c002-b17f-4f97-bcf8-fbdf640e88cf
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6854d2b6-75de-46c2-8518-a269d4e1a480
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 818
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0c8f143-b7cc-4dbf-8389-d01d47e78648
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39f43653-c8e7-4ba8-b128-a2fe1429a1b4
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f327b285-bd46-4ed9-bf62-0563b0a22d7d
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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: 63f75d5c-d21e-4087-a496-f9fc28b9f0ad
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 798
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 74c2c46f-5d63-4fd5-a78b-b32dba64fa34
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 744
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 51476370-19aa-4a3e-ae19-f0fd6ac5a7a7
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 801
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1fd21e68-a8dd-49e5-adca-1a53fb0799f8
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 745
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3781d3b9-7991-492d-93e7-33f1d29ab002
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 791
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a1be2fd3-04aa-4036-b97c-afacc99233e8
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 769
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8c16bbab-e8bc-4ffb-a1a6-e4549d3ed1b3
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 788
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8a9b65a6-db6b-48d6-ad9e-3445f9adb069
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 759
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b62f43af-cd89-4ed2-a3ec-bcc446d4c41a
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 847
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e57a18e1-5166-4fec-8f17-fd197acd6ff0
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 777
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0631462e-acec-42bc-ae5e-a6d3d800f0bf
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 763
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e480b1e7-6aca-4867-9e73-dda2fd884abf
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 757
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 64c456ba-dade-4be4-9618-c55e01a2fc81
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 789
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 173668a5-733a-4603-abd6-63d14ca68cba
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 821
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6e90666d-c830-48fa-9f70-6c721439fd06
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 748
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 313aa24d-83a2-40d7-beba-fc896831cd93
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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: fa89021e-f90f-43b1-a621-d9d1b2be9ced
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 816
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f92b5ac1-84a5-4749-b932-de76c96d0f23
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 760
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 853fc769-3366-41e2-9bb6-9461144d6b69
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c41f50c7-9a2b-4f81-8bcc-fdd9618156b6
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 772
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b6effcff-212c-4c3d-bdc0-9faa3756aad7
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 823
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fbfea3ca-c269-4631-a0ee-62791fc625a8
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 770
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7d9d0ae4-57a7-4036-850a-fbd178ece261
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 742
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 27a2c138-4a93-4e6d-988b-db62f9226ffc
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 762
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8a0b4af6-1325-46f9-9d5e-d163aa01e209
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 743
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 72cdf42b-c454-4027-8466-625fc67095df
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 792
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8927021-a6b4-47d7-aa15-963109c47939
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 747
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aadae704-d068-4182-a34a-7f12aef71054
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 740
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aae7210b-7679-4f49-831d-7dd13d8bb3a5
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 832
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bbc6e1d0-7907-4500-9061-3cb9f5e577f0
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 752
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 115005d1-6894-48fc-bf60-85c7e25a81b3
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 831
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d84b3de6-eb78-44ca-b2de-9d11aefb15ed
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 799
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a388d2c0-a00b-4d07-a44f-01503b8ada7d
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 749
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 958bdaf9-6f2f-4f3f-b601-3cc26a8eeddc
    creation_time: 2024-04-29T11:01:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe031_power.opt_pso.opt_rmo.opt.i: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
      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/safe031_power.opt_pso.opt_rmo.opt.i
    file_hash: 740668a6bdee7f1177df0d0d81e76f2a2521fb58ce5f63a4942f3d36e11f9dad
    line: 825
    column: 3
    function: main
