- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63e2b280-4a8e-4fe4-82a8-5b843c3a8027
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9dd7d70e-4795-425c-a0e5-ae2f1ee01554
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8411aab2-6f51-4de6-881a-c6b1fa25c3ca
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40ce9c0b-fbcc-48a0-af43-c5cc8a2818d0
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29607821-271b-46df-ae72-b3688c9b16a0
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17cc585b-704b-478b-8cb1-fc789b4cd2f0
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3f98967-981d-4a3c-8a88-dca48f07166b
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0
      <= z$w_buff0) && 0 <= z$w_buff1) && __unbuffered_cnt <= 0) && x <= 0) && x <=
      2) && y <= 0) && y <= 2) && z <= 0) && z <= 2) && z <= 127) && z$mem_tmp <=
      0) && z$mem_tmp <= 2) && z$mem_tmp <= 127) && z$w_buff0 <= 2) && z$w_buff0 <=
      127) && z$w_buff1 <= 2) && z$w_buff1 <= 127) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff0_thd3
      == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) &&
      z$r_buff1_thd3 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && z$w_buff0 % 2 == 0) && z$w_buff1 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0
      == 2)) && (z$w_buff1 == 0 || z$w_buff1 == 2)) && ((x == 0 || x == 1) || x ==
      2)) && ((y == 0 || y == 1) || y == 2)) && ((z == 0 || z == 1) || z == 2)) &&
      ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 781d8cea-2724-4814-b24e-713bce524213
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0
      <= z$w_buff0) && 0 <= z$w_buff1) && __unbuffered_cnt <= 0) && x <= 0) && x <=
      2) && y <= 0) && y <= 2) && z <= 0) && z <= 2) && z <= 127) && z$mem_tmp <=
      0) && z$mem_tmp <= 2) && z$mem_tmp <= 127) && z$w_buff0 <= 2) && z$w_buff0 <=
      127) && z$w_buff1 <= 2) && z$w_buff1 <= 127) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff0_thd3
      == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) &&
      z$r_buff1_thd3 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && z$w_buff0 % 2 == 0) && z$w_buff1 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0
      == 2)) && (z$w_buff1 == 0 || z$w_buff1 == 2)) && ((x == 0 || x == 1) || x ==
      2)) && ((y == 0 || y == 1) || y == 2)) && ((z == 0 || z == 1) || z == 2)) &&
      ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2a228c1-2a16-461a-8324-aa4c94ec19dc
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0
      <= z$w_buff0) && 0 <= z$w_buff1) && __unbuffered_cnt <= 0) && x <= 0) && x <=
      2) && y <= 0) && y <= 2) && z <= 0) && z <= 2) && z <= 127) && z$mem_tmp <=
      0) && z$mem_tmp <= 2) && z$mem_tmp <= 127) && z$w_buff0 <= 2) && z$w_buff0 <=
      127) && z$w_buff1 <= 2) && z$w_buff1 <= 127) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff0_thd3
      == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) &&
      z$r_buff1_thd3 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && z$w_buff0 % 2 == 0) && z$w_buff1 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0
      == 2)) && (z$w_buff1 == 0 || z$w_buff1 == 2)) && ((x == 0 || x == 1) || x ==
      2)) && ((y == 0 || y == 1) || y == 2)) && ((z == 0 || z == 1) || z == 2)) &&
      ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41f71853-7047-49fc-819d-ec04c7fb146a
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a41f1d52-b313-4bc7-b94b-ac7fc29e4e5d
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9282e9b6-16e7-4b40-8919-a71bee36f8c2
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    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: 56c884e2-401f-4bb3-8a7d-cc69a6bcbbe3
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a77cab24-8ddd-4fcc-8042-eac748971599
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ce10ab9-9df5-4078-a56e-dbe9aed25b64
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 483cde73-1e34-401b-97e3-fa752a880b67
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 253693fc-8f68-42df-8864-1036e7f846b3
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d572e04-1b07-4cef-969e-c3fda8ae3159
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71e0044c-f0a8-46ef-8d8e-90d54b1fc3b9
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71860581-a7c1-403f-83b1-871bd7d6df24
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 619052e3-5152-4eb5-a23b-e28535d7f618
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14846497-eff1-4a4e-b96a-e083a599ce87
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8de91bd8-4c7a-4a40-8ca9-0fdf524716aa
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f7bd01c-984d-42ba-9698-d35d45809d8c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3d5e3ac-6de2-4218-9733-93cbd727dbe4
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 519b351a-24fb-40eb-8615-9d2c605a5b3b
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    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: 2e61dbd4-ae86-41f3-a634-4d1c666a969c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    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: 304fa011-14cd-4372-9354-027051d9cd58
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z$mem_tmp && z$mem_tmp <= 2) && z$mem_tmp
      <= 127) && ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcde5a8f-0423-43bc-a1eb-3d2052be09ac
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z$mem_tmp && z$mem_tmp <= 2) && z$mem_tmp
      <= 127) && ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e8a76e6-6b79-4e05-af27-de84e4f220ff
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z$mem_tmp && z$mem_tmp <= 2) && z$mem_tmp
      <= 127) && ((z$mem_tmp == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e139174-7da5-41ea-b61e-6a300a6a8dfc
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c75ab35-ed87-43be-835f-dd844b741479
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67bf82c0-50cd-4526-bb19-6773dae6e3ed
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c86250d-9c1a-4557-bfbd-dc32a7498afb
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51d4b509-77a8-4c40-b99d-f60a31bea4de
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc816333-f858-4ff9-a69e-0ccefe054dc9
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 639ae018-378c-445c-8893-42147fc47445
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b85d0010-2432-4815-9922-d5ddc54705e8
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41c8076f-d34f-433b-a8a5-cf876a403533
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4ccf1ba-8a48-48b9-a687-587a0f9b4553
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0286c132-402f-461b-ac9e-86ce81e93d30
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbf1da70-ff08-4724-b517-c338a9765bfb
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c3ef78f-8768-4fd7-9896-69f7deb624f8
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    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: e4040b82-aecd-404b-a33d-997afcbbcbb3
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    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: 236ea350-6422-49b7-a390-2c754c191b66
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    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: 8f0782eb-439a-4116-a228-3fc2b81633ee
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bd52c2e-7e1a-481c-8cdf-3bef9c8c1e4b
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 821
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3ca49cd-2867-43c8-9f92-4b399687b2ee
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 18592b80-6229-49a8-99a9-3daf5cb10ac7
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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: 67c03362-d85a-40b1-8953-9dd3a7d9ad2f
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 789
    column: 3
    function: P2
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9980d0d1-f8eb-4afa-afeb-7a30a0c7bc9f
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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: 21ec4cb0-47b1-4af8-9ee1-20dfa928ece8
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 817
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8a892c33-52b2-49a8-9bbf-d0bc71025b8e
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 787
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4435d8bb-2456-4a08-9369-8719a0b6e90d
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 759
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f2740f4b-6a67-4bca-9626-edf77eadf9f4
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 753
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 48f1e20e-ec55-43d7-92fb-ef661c82cc38
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 802
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1c916020-2ec4-42a8-8910-d12d094fbc3f
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 848
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 296e6ca1-4945-4dbd-a9ff-4428af9f3217
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 752
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 856abb02-f9db-47da-a08b-1805a2e9f22c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 772
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1b0d8ca6-55cb-40e6-bf4e-ef69b562a197
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 780
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5241dbda-7693-4416-9eb1-c6472baa0b26
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 824
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aa0800a3-3620-454c-a254-7294d3b4e177
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 773
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9a4fb319-8c47-4e3c-9bfc-566e19431543
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 826
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0d3e3c23-4757-4132-a53f-8b468a4a3de5
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 832
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0f80ca43-7c3d-48b9-b96b-0cac4fbf2529
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 790
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e8ef8efc-b3cc-45e5-8731-f0ba219005d9
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 767
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0745e6b1-a81c-45c9-8448-c3f323052a9c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 800
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d5cffe56-1c9e-4f75-8400-4c11aa47d88a
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 760
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b7db9e5f-ee7c-4c26-8a18-2be286385e5e
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 779
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a40ba6a3-460a-4313-9d9f-15a1ec18a635
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aca0b886-e33c-4594-a607-612c3abd0b80
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 792
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2101354f-589a-49dd-879d-3193a733f001
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 799
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d628ee4-d2d2-488b-9a9c-a02269c37c08
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 769
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0b6ccda9-b1f7-4e79-9ef3-d1400c67d5b6
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 782
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c6f42bcc-ccdb-4a04-8f14-21b5d730331c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 822
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 33f2d4a8-cc8e-45cc-a905-0c0e42f6475c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 738
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 19ab2fb2-9803-4f90-97f4-263125f701ea
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 749
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7933687d-b479-492d-a3e1-4586f3acb8ad
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 793
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b71aadc7-2a43-4744-8637-dbc5e28c7372
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 833
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b2b81c17-14e1-4d91-83dd-6453be8e37b5
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 770
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4fd9b193-1d87-4040-9f13-dd2de2c8cb08
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.oepc_pso.oepc_rmo.oepc.i: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
      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/safe030_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: bd5019d3aed54929cd262296b7eb8866c696444f31311cf49176222c13f665a6
    line: 762
    column: 3
    function: P0
