- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26155286-ce4f-46de-92fe-9d381986c757
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5567565-6425-41f7-9683-022f869c9714
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4503f6e2-48b8-4ed0-a326-ed07af82723b
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99d322d1-3e20-4ec0-9097-9f22c4e36b75
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a926ad0-ff8f-4435-b0a1-76b8859de911
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 720fd0f7-3f57-4843-aa94-06b376d9bcb7
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d35e403c-b125-4384-af8a-757ede016d33
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1596ede6-8e4c-4803-88e3-6196960bdcb2
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 287d62a6-165c-493e-9d2e-07349a1294c1
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44e419b5-a38d-44f2-ba1c-d904b4341ef8
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ef6fed3-8d2f-4cb3-a0f9-6df7c72cd81d
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28273bf7-dd1f-45ce-9a3e-f580ad8c8fce
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f0ec650-c365-4838-8935-28c31012fff2
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb36a312-dfa5-4da7-acb5-391a92e412d2
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d86f006-bc82-436e-99ae-fb6ef2eab00f
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e54ee1e-e4a9-4de2-b544-04a8a276e4c5
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b07a781-3656-4d29-9622-36577047a47f
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a07c124d-d860-498a-b468-953a1df7e6e0
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9964e741-9d12-4757-b0a6-c7c1cb338fc3
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31700b5d-4dff-4742-9a0d-ade64f4ca053
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ab66224-2a7e-47f5-8ed8-5b7f623079ea
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c0696d3-e11d-41c1-aedd-17ca0c3171c0
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fed5880-e5c6-4e44-a875-4bc3cfc2f43e
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec8d43e4-3f78-4389-820d-895579a73110
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9217dda5-438d-42f2-a352-4c6538ace09d
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 034ad040-2c8e-4abf-91fb-fab1ff97985f
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bca75682-9a0c-411c-ac6f-82987bd27a28
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18f268c3-3cec-46f5-a703-54204e5f7e8c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e3d5b60-c5b9-4e10-a34e-5c699242a3b0
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fa32846-2b56-4733-b4e6-3f4bd9bceb3c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6380abd8-64dc-42f4-bd50-3ad9a2980c8c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4354df42-744e-4d32-a805-ea3c5e2b20ea
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0657997-8974-4458-8f78-24ec7bb3043c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8715a7af-d72f-4613-bfb2-37bbd3160f8d
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && __unbuffered_p0_EAX$flush_delayed == (_Bool)0) && __unbuffered_p0_EAX$mem_tmp
      == 0) && __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p0_EAX$w_buff0 == 0) && __unbuffered_p0_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p0_EAX$w_buff1 == 0) && __unbuffered_p0_EAX$w_buff1_used
      == (_Bool)0) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) && y$r_buff0_thd3
      == (_Bool)0) && y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) &&
      y$r_buff1_thd2 == (_Bool)0) && y$r_buff1_thd3 == (_Bool)0) && y$read_delayed
      == (_Bool)0) && y$read_delayed_var == 0) && y$w_buff0 == 0) && y$w_buff0_used
      == (_Bool)0) && y$w_buff1 == 0) && y$w_buff1_used == (_Bool)0) && (__unbuffered_p0_EAX$read_delayed_var
      == 0 || (__unbuffered_p0_EAX$read_delayed_var == & y && ((*__unbuffered_p0_EAX$read_delayed_var
      == 0 || *__unbuffered_p0_EAX$read_delayed_var == 1) || *__unbuffered_p0_EAX$read_delayed_var
      == 2)))) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (x ==
      0 || x == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((y == 0 || y == 1) || y == 2)) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 621af203-7dd3-49e8-81d2-4267c703a2a2
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && __unbuffered_p0_EAX$flush_delayed == (_Bool)0) && __unbuffered_p0_EAX$mem_tmp
      == 0) && __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p0_EAX$w_buff0 == 0) && __unbuffered_p0_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p0_EAX$w_buff1 == 0) && __unbuffered_p0_EAX$w_buff1_used
      == (_Bool)0) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) && y$r_buff0_thd3
      == (_Bool)0) && y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) &&
      y$r_buff1_thd2 == (_Bool)0) && y$r_buff1_thd3 == (_Bool)0) && y$read_delayed
      == (_Bool)0) && y$read_delayed_var == 0) && y$w_buff0 == 0) && y$w_buff0_used
      == (_Bool)0) && y$w_buff1 == 0) && y$w_buff1_used == (_Bool)0) && (__unbuffered_p0_EAX$read_delayed_var
      == 0 || (__unbuffered_p0_EAX$read_delayed_var == & y && ((*__unbuffered_p0_EAX$read_delayed_var
      == 0 || *__unbuffered_p0_EAX$read_delayed_var == 1) || *__unbuffered_p0_EAX$read_delayed_var
      == 2)))) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (x ==
      0 || x == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((y == 0 || y == 1) || y == 2)) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32c8d933-e7b5-4d29-aa7e-a29b1eec3b77
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && __unbuffered_p0_EAX$flush_delayed == (_Bool)0) && __unbuffered_p0_EAX$mem_tmp
      == 0) && __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p0_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p0_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p0_EAX$w_buff0 == 0) && __unbuffered_p0_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p0_EAX$w_buff1 == 0) && __unbuffered_p0_EAX$w_buff1_used
      == (_Bool)0) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) && y$r_buff0_thd3
      == (_Bool)0) && y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) &&
      y$r_buff1_thd2 == (_Bool)0) && y$r_buff1_thd3 == (_Bool)0) && y$read_delayed
      == (_Bool)0) && y$read_delayed_var == 0) && y$w_buff0 == 0) && y$w_buff0_used
      == (_Bool)0) && y$w_buff1 == 0) && y$w_buff1_used == (_Bool)0) && (__unbuffered_p0_EAX$read_delayed_var
      == 0 || (__unbuffered_p0_EAX$read_delayed_var == & y && ((*__unbuffered_p0_EAX$read_delayed_var
      == 0 || *__unbuffered_p0_EAX$read_delayed_var == 1) || *__unbuffered_p0_EAX$read_delayed_var
      == 2)))) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (x ==
      0 || x == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((y == 0 || y == 1) || y == 2)) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc8657b0-ac39-438f-8460-d7b350d27402
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1336bd5-eeeb-454c-89e3-d0bc80bcb486
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33dcc298-a265-477d-ab8d-c897c6836008
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19797606-db60-48b0-a925-8c90447a6384
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8130c9a7-4548-4d2c-8e63-1337acff5e04
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11238ef3-2cb6-451d-ba38-f0f4203bb3aa
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94cb1848-fba5-4bd6-9cb1-23c6be02d83a
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c68f546-bddf-4034-a567-10485f84d0bc
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 379c20df-b3f2-48a4-a654-9d1f61dfac53
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0225428-f649-41ee-89ad-a323ed8f4ee7
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed_var == 0 || (__unbuffered_p0_EAX$read_delayed_var
      == & y && ((*__unbuffered_p0_EAX$read_delayed_var == 0 || *__unbuffered_p0_EAX$read_delayed_var
      == 1) || *__unbuffered_p0_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e4cedae-177f-4de3-97c3-eac881ff6523
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed_var == 0 || (__unbuffered_p0_EAX$read_delayed_var
      == & y && ((*__unbuffered_p0_EAX$read_delayed_var == 0 || *__unbuffered_p0_EAX$read_delayed_var
      == 1) || *__unbuffered_p0_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 518be2ba-cfc7-4580-8a8d-8ddb88c25623
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX$read_delayed_var == 0 || (__unbuffered_p0_EAX$read_delayed_var
      == & y && ((*__unbuffered_p0_EAX$read_delayed_var == 0 || *__unbuffered_p0_EAX$read_delayed_var
      == 1) || *__unbuffered_p0_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72de6b73-ba04-4690-85de-769132e07f45
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa16efd7-0a5b-44ae-8c4a-a8c52d94c367
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2354e39-7781-4d83-92d9-7e27991785e5
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3284ed81-689c-4953-9f59-5d205aa371f1
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 660aeb8f-79a3-43ae-884f-6fdfe425772c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9ee51a6-8688-4b92-a181-eb484c90a6c3
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a88bacc8-9b4b-4599-9b21-15ed3dfb58ef
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4e19cc5-cae1-418e-8a5f-f8beab877281
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a18a3af2-2b98-4823-b725-25adc60e8580
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1532e0da-9b6c-4f69-a12c-8719db5c9e7d
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf7cfd1e-dab2-4914-ae07-317fd8312708
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef0a6c51-a956-4c38-8065-ff16b4cbac91
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4dadd6d-9607-4e70-81e6-f3754fa9c0a5
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 192506d3-581e-4a4f-84a4-60aef80f4f91
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac05a626-f3d6-464e-9785-f54d7fc818b8
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 048b5fb3-ab83-4b84-a7eb-db3411ad9607
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 806c2e7a-0386-4fa0-9b5b-9e6f53c13a9c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db9389c1-a6b7-4ee5-a7ca-6b32a3fa6ba3
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5673a981-a5bf-46f8-a8f5-ff1b927bddd0
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f301c07-519e-4a0b-817e-430e6b6f4079
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65c35a81-a112-469f-a81f-5e556052e8fc
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be342706-6512-4db6-99b2-b4f4c30d6919
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9112c9d7-1585-4db2-b068-85b00f6a12e5
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e076fe3d-2a91-4c31-a08d-ab581a15fa48
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83c8892c-ccc7-44ce-bb49-209aee0f6023
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1) || __unbuffered_p0_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cd607a4-23f3-444c-92d6-9353fd0b2223
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1) || __unbuffered_p0_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5504e40b-6fde-4818-8d8d-eecf300bf367
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1) || __unbuffered_p0_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7869d32b-38ad-4cb3-b8c0-b01b06762b60
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dad135f-b980-49cd-94e0-f0dc0b8028b3
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d58777a-1cbe-4529-a520-913e1f2734eb
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7279f89d-1928-4437-864a-0be8b48fde67
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cbe6501e-781a-4f2f-bd43-51ab36e636fa
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da57c05d-69f6-48c5-a221-930f51fc4d4a
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f7a7839-7f58-45d5-ada0-3257d01a26eb
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ad72c60-d7a4-4980-ba46-2c0ffb05d654
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf7b778b-243f-424d-9066-dec40ea19f42
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcc17e20-9deb-44e2-b6ef-bb8c47170bd8
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e6c78da-552f-493c-bd05-0905745c8c9e
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9963840f-906d-4c0c-812a-a7d127094ab1
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88f7a8d2-33f9-4900-ba60-49a1acb28683
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7143bb8a-f3ea-449b-aff7-35b965533ee6
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bce544e-959f-4dbf-b86e-4a471b6e9f76
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a296ec5-3999-4f51-a2e0-3c9a26a2b341
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e82fe977-d56e-4fae-8b77-c242560562be
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb180ec4-e2dc-40d2-b930-a053fac10713
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f8857ec-ce4d-476f-b47a-250a5b4f6801
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29ff7f03-68fa-40cf-a559-c97206d750a8
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: faa7fb7d-6b40-4847-9485-5b44b6615ff3
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4e2ad48-7f9d-4ae7-ac3e-a263549924c5
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47a54cf1-bf56-4383-81ff-15879fcb9207
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00b69ac9-4c07-47e1-bb42-2678dd52f17d
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d5608cf-7b42-4878-a6c6-832ce0784841
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bacf6369-941f-48a6-b9d6-442c7537f87c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2d1decc-e194-41bd-ba4b-7ddbabfdecf7
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5223800c-b81c-48f3-a6f6-5f3195a7c812
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y == 0 || y == 1) || y == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11de450b-8829-43bf-bcf0-f6c5f9d7a5b2
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y == 0 || y == 1) || y == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e88f87f7-84e8-443e-9bc7-2ce99d75e9de
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y == 0 || y == 1) || y == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d7d4a80-be02-42ac-aed5-0bf1cc5a8888
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 838
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42e9c72b-3ba4-4db6-9c19-7be78ca67d68
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 840
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a85fbaf7-507c-45bd-9e20-3728a0160c71
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 841
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 3a9d7642-e3d6-468f-a9b7-327c962bc19c
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e6c825eb-2a4d-4e07-8ecb-4f3bce49bd77
    creation_time: 2024-06-19T11:47:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe009_power.oepc.i
    file_hash: f20fd36bba02e157a8b8bf1ebc392e6f77e4774b666ec7e51005ea908400e881
    line: 836
    column: 3
    function: main
