- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1796c564-1e0b-40a8-a622-cfe91974a864
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c94effac-c20a-47dc-89d7-5b8be9dda2c4
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ebb08ff-fe61-434a-8026-b7898e67a481
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 072db688-4456-49a9-9519-f23915d11239
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: a42d6f03-40c2-4727-a2a0-f597619dba17
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: bc1b5896-04bb-4ece-9ac0-024b1dee4862
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 28fe7dff-229c-4237-b9d2-4ab2e6afa4e2
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e89e4106-94a3-4b50-ac95-f9521c88404c
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c093318-c51c-4931-96b2-8ab238a4efd1
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d36afbfe-d54a-4fe9-b9b1-5c38d2cefa0a
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 0e8f608a-cd1d-450e-a5dc-a32fe30caeb4
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: cdad3b28-3a63-4951-b527-8ab3da760a82
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 0ab1d8df-c088-42d7-abfa-f7d6bb2866ab
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b99d85d6-9da3-4950-acba-5adc2361f69d
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d791ec0-4d89-49bb-bfde-0e62c75bcb71
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1ff93eb-aabd-4d34-b276-407913faf0e9
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa26fc9f-931b-4e4d-9f8e-205bf9918245
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbb213bb-d0d7-4053-a20c-ae0c0e3a64bd
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd20e11d-457c-4925-af56-823517802508
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 92b4d2c5-62a2-4a10-b050-2e01f3feccf5
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: bf081b46-4f69-43b5-b2ff-e5e0b0dd4cd2
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: dc00eb29-cdb1-4f07-9387-6158594d29c8
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba9780e6-605f-43ea-83ba-a5f76897727b
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ef6beb9-739c-4b7d-9ccb-cf1ac8d672b9
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d5b79d7-be84-4b63-a5ff-d6e579e330b5
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 7c81af6e-025c-4a69-8941-b181178ac564
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 80f519bc-b3d8-4d73-b5c5-a93213e0d09a
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 02f9fb74-9406-4c6b-8e5b-d24980f3dc9e
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 087ba35d-6858-4f28-866d-0df2c8df6226
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 579c128f-3b3b-44eb-bbc9-1eb4e24f3ed0
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 046eaccd-bd1b-4bdf-bb0e-b37bf2d5bc6f
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: e7bdbac3-d018-4a1a-ad02-4265f28ed0e9
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 976574be-c2cb-40ca-913a-3acf1ef75cdb
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 8d32a3f9-595b-455f-af4f-ac69c469aefb
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || z$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f95f2c4-ee3f-4bd0-9c33-284035e46882
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || z$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f810429-5b97-4b00-ba3b-12e14302f397
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || z$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5511777-7008-453a-94ff-cc69263d4757
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c658389-7193-4d2c-af96-c2491522328d
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2e285f9-f97a-4c2a-9f1e-9e15bb2da5bd
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b5613cf-9afb-4724-abc7-6853188ce3ea
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: f59737e4-d02d-44ba-96b8-5e7516787a05
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 69f06537-3f20-4deb-a769-4a772de894b3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: e355aa83-2230-4983-b272-4a9ef15b4810
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6bcd302-284f-404b-beac-cdfdb4b9a6f0
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbbf54bd-3ce1-4641-8c49-27a3e207c9b6
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed521d34-4553-4dad-a4ce-2369fc4cb69a
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 596cf931-f3ce-4f01-be0c-40aafc6068ae
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 345763de-606e-4667-913e-ed4b9087c884
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e718ef82-c73d-4fbe-a8b8-f2e0876cca7e
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0af34ccd-b64e-4927-af46-ed6967fba972
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0847a587-5a50-4eee-b203-4a8e61b38dcd
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c84e8ad3-234b-47e5-83fd-b117e59bd901
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 2f8bab82-ab19-4229-a75d-197f39283eb0
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 630412d3-7993-4c78-98d3-b8f92f499ca0
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: a0411bf1-403e-41d6-9e73-0ba96dac9378
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 823e62c8-2f2e-4b14-8500-76ca28f5351e
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 95c5012a-8cf8-4a46-b229-746000974dfc
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: e839f6f6-4159-4ff1-852f-8b9bfa127f93
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 1659fcfc-eb19-4bf1-94e9-067feda047be
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 25c9bbf0-cb4f-417d-b532-86655b25baae
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 9c939b71-f869-4621-8187-2b39db0652e0
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: a9bfa302-99b2-4abf-8d33-789e61294ef6
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: fc6cd865-e94c-4b0e-ae8a-aa4c0e103c02
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 8287a46b-e50f-4b30-869f-726769b3beaa
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f99715eb-d28f-4b70-b3bf-d2dd1950098e
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5ff8a1e-0afa-4cc9-af3f-5b1fa032f5d3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46edb861-c3c9-4c87-9bf8-dff3af205ef9
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: e9a592e8-4b9c-4f61-9dc2-2633340fde5d
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 3230e8f5-ae31-4058-9019-d89384bdbaa1
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 555b2c73-73be-4b66-afcf-169f8c13b527
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: f6739bf1-6365-4652-a105-16ef1af897c8
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: a5218b6f-f8f4-453f-8e91-25ec1a627880
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: a093c75d-866b-471a-aaf7-41205a093fa6
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a662d49-8fdf-4601-9ed6-46a7d0365936
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68e5c698-15f8-4828-a64e-a4c4828b382f
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad392953-2ebc-4fdc-9f32-9128e966ad1a
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 9727ae0e-7e95-40cf-95a3-c06ba548d7ee
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: dfb55f14-e554-4df9-a1f0-d42941464014
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 5c26569f-df63-4fcc-a448-92422b51ebb7
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7bd6fa3f-155f-4699-b7a8-b7875a044d72
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8916bce-5885-4609-a8e5-0eb3dab764aa
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27a3388f-9d8e-4395-a033-d2d84d89b0b1
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 5a3c8e04-20a3-4f46-8e0f-bbccbe22d425
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 9682e33d-3ccb-4223-97dc-962e4bde4de7
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: 917ae4b6-b535-46ad-8db5-aa8a19c99161
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 609df2ff-ebf2-4d7a-9d63-03692b43b089
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: f8ab7304-c027-40a1-868b-1647ce7569f5
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: ffd15c35-21ce-4754-8941-4f12d91a9e3c
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82676d5c-21e3-44ed-8110-786f500128d3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 174c621e-6247-421b-8785-5d7507e80f03
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bebd53b5-8f43-4538-9d5e-ed2f10afe28b
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 49f3fb3d-f677-451c-b6d1-012e3ebbd6d5
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: dc2cda8e-4902-4b89-a0f3-f97cd99fed7f
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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: c231490a-f2ff-4b76-a630-89240072eefe
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25bf88ae-a338-4a84-8cfd-79185c56c537
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be4dbebc-0198-46c9-9f17-f29c9e260c69
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76a0fcb7-a946-4a29-a2f3-46b18930d599
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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
      <= 1) && __unbuffered_p0_EAX$read_delayed_var == & z) && (*__unbuffered_p0_EAX$read_delayed_var
      == 0 || *__unbuffered_p0_EAX$read_delayed_var == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c537874d-b323-4edf-bb81-8e699f779933
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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
      <= 1) && __unbuffered_p0_EAX$read_delayed_var == & z) && (*__unbuffered_p0_EAX$read_delayed_var
      == 0 || *__unbuffered_p0_EAX$read_delayed_var == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfa74e1a-4ea8-4cde-b48a-519ecc140716
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    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
      <= 1) && __unbuffered_p0_EAX$read_delayed_var == & z) && (*__unbuffered_p0_EAX$read_delayed_var
      == 0 || *__unbuffered_p0_EAX$read_delayed_var == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ee7f008-532c-42f7-8d02-78de808a54d3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d4b893c-21d0-4fc6-b128-96ed0462375f
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7df5ad75-dd01-46f2-945f-85ed27a17e2a
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b5c749d-9674-44be-907a-48643102805f
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3c62a60-8189-43e6-afa6-1d595b2e561f
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d65bfce-994e-4b7f-837e-31038bc37fcb
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ad5cd29-8b29-438a-8e50-a6155fcea4b8
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12210ab4-4c21-4602-bf39-c259c7bcfc6d
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98ff5c37-9ff4-4cad-a8d0-48a0e9b5c4c1
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5762c1a5-0f98-425f-a018-032a1ac0e564
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 300771c7-14d3-4624-970c-db6f73327471
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c006ec66-b8eb-40bf-b89c-c643ffbb515e
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9916c55d-f69d-4507-a4b4-bf79550836be
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    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: 18ae9288-fe0b-4bac-baac-a6f86063caf1
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 842
    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: 4dca4e27-96d1-40ed-bd19-3d10024b3849
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7a881cc8-e34a-4b96-91b6-b5bc73317a39
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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: 27ca370b-a1bf-4b45-aa93-043c979ee73e
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 780
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 597f1940-63e6-437a-a52f-60657b7c72c3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 796
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2654b801-dae6-4276-a0ae-d41434fd0a67
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 781
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4440a78d-8223-4fae-b43d-86a492c080f5
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 800
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1b6633ee-7d25-4bf1-9e0f-8d5d90c3426d
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 823
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4bab71fb-3703-429f-9490-9c1e2206826d
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 821
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf2be638-d2bc-4781-8e8b-b58c391b8a4a
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 810
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e7774f3f-b3ba-4e3e-be4d-7a44a6e925b3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 847
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 67c12bcf-6718-4359-8602-32449bc15c38
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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: 08307ea3-4861-49f9-9527-2980ba844307
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 838
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 62be89cc-68c5-4e4b-b518-92f8e94f90f3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 786
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b2afaec8-cbac-456f-b71a-7f7e1e1aca85
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 788
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b7695e96-2187-4538-8179-551bafed6923
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 803
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 93f1391a-77a3-4426-b1d5-04e0d9e3da0b
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 845
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 49f0f080-17c7-4622-abce-debbb540d956
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 784
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a3b6d984-1d7d-46ce-ba50-16863c0ade2b
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 811
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7dbeaa49-e426-4ac5-813f-4ad7d107b508
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 814
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 500ea6c0-e91f-4cef-9e0f-7c9ef2168abe
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 808
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d65e74bf-36f6-4bde-b85c-5192b9c0634a
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 783
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a8c7b745-22fa-451d-9d24-8ec7aedaaa81
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 813
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d7aa4b78-b591-4214-9d0b-78d7c2b56d1e
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 798
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 38b879b5-faca-4036-99cf-a4ff8575ed15
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 843
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8cf06cfd-fe92-4e75-96a0-c857820fafa3
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 795
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a375da53-826f-40e9-b9d5-d25cdbbd1899
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 853
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8f1940fc-1082-40b5-a76b-26944137eeba
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 762
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2474d59c-c3af-438f-9404-4d6fd4d76737
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 820
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a7675ee1-5333-4f9d-a2aa-a904331e8ad7
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 799
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 39b0366a-1b01-447d-9da9-d49eae89aabc
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 793
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b2545019-578f-4a9b-82a6-6e9ffc1dcfc6
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 854
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9b933987-13e9-43dd-988e-dd758ca46ada
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 801
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 53d5464e-dbfb-4c3b-9341-50def0012573
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 785
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8b398c20-9aab-4211-b145-c1514ce30b13
    creation_time: 2024-04-30T09:37:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.oepc-thin001_power.oepc.i: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
      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/safe007_power.oepc-thin001_power.oepc.i
    file_hash: 51eb1f25b31a14b06f8a94357507f98faff1b5d262be3400ea1666eb362dde3f
    line: 858
    column: 3
    function: main
