- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e1b132b-332a-48b7-94d3-1f26db39b36a
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 311ec47d-05c5-4d48-a547-ecb754c12ffc
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1a24b25-87c4-493b-8795-d3f7dd9fd595
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f300cc8-1463-4e68-9c4c-ab59cc0f4241
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6eb04b2-70dd-4c9f-8f7d-a9bc30e6b91a
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 965eb7d5-1012-4aa3-b17e-356886c587f2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93d2601c-3bf2-43ee-89e7-cd4cb3999e6b
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11bfffe3-6ef5-4db1-ac4a-8b26ee5f7ac7
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d0678c4-d932-4436-a1ae-26554664af84
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 169b099d-18ea-48c4-95ee-94c20aa51978
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4528d6a2-54f6-4404-8f9a-c9a91c4cd54f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 133653d5-91e1-4792-aee4-31d5596f1ff1
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c410a3fe-d725-4c76-8982-dea83c8f6caf
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 990e393a-46c4-421b-b504-c9aa282bed83
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0f7c31c-1bdb-412a-8026-de867a369987
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4703aca-0be7-4c35-b896-936f1f7b6225
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aad61a1d-39e8-4f5d-b6d3-2b72208f3a0f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5922c320-7145-4fbf-8179-afdf97cb6bc5
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24b008b9-7f98-45a5-8822-b196703e1e04
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0b57b6f-e86b-4a60-a3f4-ea5b4a2d53ad
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f31e2f39-10ae-44ea-9709-70f03083a0f2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0af7e44-c530-48cd-bca5-b0e4b2df316f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 805b3878-68fc-4ea2-8e1d-1a352d9b8711
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0120ce49-fae8-4892-89f3-2379b63e5c47
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05d4955f-f6cc-40ba-ab83-61534bdc8af4
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3fb0adc-d056-4799-ab0e-4afc6e21ddd1
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 101e9bcf-2a16-4062-8da6-415729eb6f56
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41c9b4f2-e866-4d8a-ae98-5c49c63f0bc2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    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: 8891a0bf-cc7d-4537-90e2-ab69b5e5b2f2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    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: c2c1a0a4-9f66-48ea-811c-9a2f64627aba
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    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: 26fd4a7f-bc01-4dd0-a4ea-b705ce8eabf8
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 841393f6-0bb9-4fbd-aeda-c68d3fcdb961
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db815468-e3cb-41a2-bcd0-c64859217f98
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fab1a0c0-31b1-4197-ab06-81c7c5f7e8d7
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0be2d8dd-8b89-4855-9ec0-a1a198eabefc
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cec68d21-b86d-4053-a323-c8456876be58
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50b690fd-cda1-400b-88cb-4bc059d9d69f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf16d853-3ea9-4d5a-8cb2-fa1704b2fa95
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 012b70d7-6abb-4305-b07c-28e79606531b
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e2a69af-7e1e-40ff-b213-5d0dbc6673b8
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd9978c3-813f-4cc7-8aa8-239424040a53
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0f9ff3f-838f-4ce3-95a2-2556f1560461
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 486c5939-c249-41a7-afa8-68a20a1970bb
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a621b927-faa3-430f-9a0f-709b0b1c8f9c
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f147d6d1-5c21-4859-9f71-3cdd4120d46e
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dfd04e7-b5f2-4609-8e3f-c0b9ac47c4b8
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c7f7df6-51e6-4a05-a0a5-0713119a3f7d
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 620901ed-c7a1-4d4e-944e-dbc1fcfe1a91
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab778ba5-aa02-4695-9e74-44b9ac1a88a0
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82e60474-8c74-4f44-a376-ccfba576f426
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90c6e3a8-c6f4-43b7-ba70-7e712da34bfa
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7408573a-7f44-44a9-b15e-169463c4beff
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 2) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2b21b85-020d-48df-80f4-0b53965e2c72
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 2) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8be92393-cb4a-419d-ad70-0a0a59f439b8
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 2) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5b274e9-712f-41a7-80b9-722080603c49
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80e82457-4326-4fca-8efd-b00eb8ecbf14
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45244d84-7cd6-4eb6-9205-b5631dc64ce6
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4798d57-5a3d-464f-b424-4cc66fb0bfe0
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3809b9a5-7abd-49c9-8c50-e8a8f10a6327
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9e9d841-9426-482d-9f40-8f411d259df9
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d29e9838-3fe9-403e-84e8-fb8a5fe90ea7
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c70f7929-af19-4e01-b9b4-a43e2b546cb2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 381dac75-a391-4035-8fdb-ec4869791d1d
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f898da3d-7c9a-4e36-864f-49aabaaae6e1
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51cab2cb-d403-4a30-a6eb-c7cba9dcd0a9
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40da8ee2-5b08-48e8-984d-996cc0ef7666
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22e2671a-e2be-4805-8f3d-9a45a0e84174
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51cbf552-8c4f-4ae8-a0b4-ce72d16a8611
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b2c8a8c-77e9-42ca-94c7-ddf64a9dec49
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 412637b1-1398-4f0c-9bcd-82d740541ae2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0cbd69e-5ed9-41ed-9914-938208ed64a3
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae483778-1978-481e-ad44-047aad828367
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38763350-9181-4037-9296-633768eeb752
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f91eab6-6e87-4f84-ba67-3c401e487dee
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80aaed55-a824-43c1-b9c6-32728288eb2c
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3114bb17-fb3a-40d4-a6fe-5fd0765fa1ea
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75bc53c6-27df-4682-9aac-724fd582ed6e
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f8587c4-2af6-467a-8856-126ce4ecba21
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1328e7f-0283-4048-8146-50b467cece79
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c87e6f04-09d4-4176-b436-657db2d92068
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf14202e-be85-4856-be75-a79c07878164
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2f871cf-7294-43f8-b90f-ce58074d471a
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a332ad9-d5cb-4ace-836b-e3005af5da3c
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28e5dacf-1609-4a02-b9c1-599dbe002937
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32b3ab8a-a115-4f18-aa6a-bf8864982c56
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed == (_Bool)0 || __unbuffered_p0_EAX$read_delayed
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6224ef0c-2794-4de1-9bcf-06f4b8ed65df
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed == (_Bool)0 || __unbuffered_p0_EAX$read_delayed
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 517c0bd6-0f5b-42f5-8ebc-e523ec0643f2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed == (_Bool)0 || __unbuffered_p0_EAX$read_delayed
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e520a17f-2051-4c5e-9e1f-074ce5504176
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    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: da9f0621-5e20-4257-a22c-de3c50d0bf7b
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    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: b06fa98f-e75d-4f17-9b5d-59ae28286538
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    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: 06b64146-bc7f-4cf6-a3d7-7a891c99b4cc
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 026bd79c-e274-4d55-8c9c-3b75d78d771d
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dd8e61f-ef9f-4eba-8c1f-2937c4327a06
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a25a4b9-f66c-414e-908c-346f79fc2a22
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 705bcf9c-b60f-453f-bb1f-7adceade6087
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee2e624d-11bf-469c-aa51-1da0c1f1e07e
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd5cf110-ddd5-4232-b78c-86e89068f3fb
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1049f4e1-7a32-418e-ac9f-5a948842c1c9
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d3edc86-f837-4170-bc0e-a70e057a963a
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51a68caa-83c4-4bff-a422-4b86dc0417f5
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5911500-432d-4bb6-9013-69fa47a25723
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 643de436-ebe1-4634-aae9-39246eb6598e
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5e9b66f-3f66-4f63-9f79-1195631466ae
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice1 == (_Bool)0 || weak$$choice1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fad3f420-3894-459d-8d9a-5bc4638d0b8f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice1 == (_Bool)0 || weak$$choice1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57efab26-3549-4acc-b184-6cdf87a34427
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice1 == (_Bool)0 || weak$$choice1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b96f6d7-5c9c-4acc-b7a2-3ed40d2af763
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12241533-a3d4-4789-b594-4a64d55aedc6
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c80d27d-1aba-4b5f-be77-68247aa2066a
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64d7ced6-64e9-4607-bbdf-c0f90154592d
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7ec7f90-cc2c-498e-9246-3bad9fd55a9e
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5635550e-7370-4013-9e58-94566171ee7c
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31b9fb10-d923-4795-bb70-05b4eae03331
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67a18b47-0ff7-4254-828c-0ebb0201a963
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecb03884-bf38-42e9-9a93-cbe6da7c8b28
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e73db98e-0f63-4671-a4ff-44da424efd90
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed_var == 0 || ((((0
      <= *__unbuffered_p0_EAX$read_delayed_var && *__unbuffered_p0_EAX$read_delayed_var
      <= 2) && *__unbuffered_p0_EAX$read_delayed_var <= 127) && __unbuffered_p0_EAX$read_delayed_var
      == & y) && ((*__unbuffered_p0_EAX$read_delayed_var == 0 || *__unbuffered_p0_EAX$read_delayed_var
      == 1) || *__unbuffered_p0_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae1cc812-22c9-4664-8a51-994ecede0cc7
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed_var == 0 || ((((0
      <= *__unbuffered_p0_EAX$read_delayed_var && *__unbuffered_p0_EAX$read_delayed_var
      <= 2) && *__unbuffered_p0_EAX$read_delayed_var <= 127) && __unbuffered_p0_EAX$read_delayed_var
      == & y) && ((*__unbuffered_p0_EAX$read_delayed_var == 0 || *__unbuffered_p0_EAX$read_delayed_var
      == 1) || *__unbuffered_p0_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6834ab18-92f1-4fe5-b715-afdb65be3fc5
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed_var == 0 || ((((0
      <= *__unbuffered_p0_EAX$read_delayed_var && *__unbuffered_p0_EAX$read_delayed_var
      <= 2) && *__unbuffered_p0_EAX$read_delayed_var <= 127) && __unbuffered_p0_EAX$read_delayed_var
      == & y) && ((*__unbuffered_p0_EAX$read_delayed_var == 0 || *__unbuffered_p0_EAX$read_delayed_var
      == 1) || *__unbuffered_p0_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0aa16b69-5cd0-4fa3-8c6d-6e0846609fb1
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$flush_delayed == (_Bool)0 || y$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50b1ddc7-bb45-4187-a186-5f7d06b1c96c
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$flush_delayed == (_Bool)0 || y$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 253b04c9-1522-499e-8d9e-f9d4951f3408
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$flush_delayed == (_Bool)0 || y$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5415c683-0ae6-4115-9856-9e199f1a27e1
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59c671bc-8f38-442e-957a-5db7b20a444b
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e80b783-0dcf-42a0-ba02-f79f00901297
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b466a460-b062-4fbe-a1e8-de4d706fc5a9
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c629bdd-7016-4eab-bc4f-117e61dc012f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acaa7eb2-4a67-4f2c-9d15-676de147d326
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb24615d-378f-42e4-ac5b-7f5b247d2566
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c15ae60-5863-49ba-aba5-e7fedf1bf377
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50eca0a4-dc87-4928-9f7b-3dbc48572ab2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6748a78b-22ea-4df7-9036-c231ef8f1ddd
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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: eee49971-78bd-4475-ac0f-1076e530ba69
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 776
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 28edad91-b499-4981-a7b1-eca10e8a9f6f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 845
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 95dec7c7-9c03-4d52-8bc5-6682ebac89f2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 792
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf87b3ab-2f01-4a93-a28d-24e6f057480c
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 812
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2ed8f894-4511-4640-a55a-816991089e86
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 777
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f55b530f-c315-444d-889e-bacba3b18358
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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: 8dbf8c22-01b2-46c6-8dd3-c580b4f68ec8
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 836
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a66244ff-3c18-4e82-82d0-06cf41a683b3
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 804
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b900e660-fb75-44ab-8aa0-6b8f00f98708
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 821
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4a6df8ca-784a-4166-a073-ad426c64ced2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 801
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d490ea61-de90-4033-884e-fc8c9589385c
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8d9088d6-c3fb-4ba9-9d99-3082441d2b59
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 843
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f26d257b-fa43-4650-b741-180fcbd9756e
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 782
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 655db40e-d45a-49aa-930b-ca076e6a2eca
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 818
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9e0b9161-89df-4947-8b4c-78822398cbda
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 784
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aea2de19-75ad-491b-8615-b4edfa3d122f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 851
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dbf8635a-9ce0-4fac-9371-4c5aca0b7e14
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 780
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 418faae4-71b8-4df0-bc55-fc3d89ebee75
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 869
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2c45b3d7-2f8c-4abc-a64c-3cba71ca1268
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 811
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8815f90f-8075-4200-8b7c-78bc0f378291
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 779
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: babda92c-d06f-47a4-ab4b-8de38e7df598
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 794
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 97a65c01-5906-4c40-830b-3616ba54722a
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 809
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 32921e32-36d9-4ed3-88a0-b721a02d1607
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 802
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c147529f-7e49-4361-8752-4d8ef03b2f36
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 791
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 696049ef-791a-4e67-ad78-23a5544aaaf1
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 758
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ef7db15f-7645-4224-baa3-3135e5912a9f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 852
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f4d27b99-05e1-4b97-bc54-9d68cf6875c4
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 795
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e0458c3e-8951-4ddc-acbe-243a624c6ab2
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 819
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 089c4ae7-0f81-4b9c-8db0-68629975889f
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 789
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 376db046-1bc8-44fd-ac0f-ac4a9cbb7bb4
    creation_time: 2024-04-25T07:37:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      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/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 781
    column: 3
    function: P0
