- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 464e9246-a109-4f57-94e6-5175c84e5157
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 3497c885-4cc1-454f-9ceb-bf528c40f438
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 9d8d7d0f-dab9-4a7b-ade3-460480c9f814
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 6f78d847-64d0-4791-862d-7e51e95116d8
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 00c9fefa-9763-4139-a322-506dfc4d58be
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: d218dc67-b14d-428a-ab78-7bac5dce6de6
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: ca625d73-4f55-455d-87d4-e74e0baf433e
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 1e9cde96-013e-4403-ac58-a3807b9b1e9f
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: e460585a-46d0-4f36-b5dd-090f94a71f17
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: dad30b2a-4bbc-4eff-9e81-f70283b64433
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 8076cf3c-dcf6-4aea-8c08-b5f3f2adaecf
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: a20caf23-bae5-49c4-a697-9ffb40ca09b5
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 9a7dfb61-af1e-40b4-823a-15bb60283944
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: c4cb6030-7698-4103-91e5-841ad86c6990
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 8717af28-c528-4cec-9673-4e8fc65b196c
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 3be095bc-6b6f-4852-926d-0c607e454741
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 234c36ee-271d-43db-9654-72a5668363d9
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 7d324603-5c04-4881-918e-cd1aa34e417f
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 2651431e-7f39-4276-9c07-c234b6b0c3ff
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 27a59b21-1231-455c-b653-a20f792c2cef
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 2a64bec4-626b-4818-bb47-20fef604ebf9
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: b1e28864-bc8c-40a8-b574-244a60ba004e
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: f24d824a-061c-46c5-a9bf-bcbc953cb21b
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: ef56dcf6-e164-47b8-ba96-192ceff548e7
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 074b0e56-c7db-4129-a364-be89df2eac46
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 5e17ae4d-6ac4-4f08-ab86-7fe819fe15e5
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 5dcf99d2-cf2d-421f-bad0-7794c5654838
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 1046eca0-0aa6-4334-9611-ff63dba7b539
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 6e807411-aa86-46d3-a794-e9d6620bfd14
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: e06c2b06-d615-426e-b4e9-26ed4ccaf1ee
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 6e8c2d32-5d3f-4b9d-881a-7e2cddeac4ce
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: d2aa212e-7a19-4f52-9ab1-e4ea7c84d813
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: bec76ec1-8b26-4584-b744-527d30329e13
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 2d865a51-4c08-4a71-9dca-62eda63b13f7
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: a590776b-62d9-43b6-a040-a00784df214a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 0160f83e-3407-483e-b53a-d4ffc855ab93
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 4e06a3b0-f6f1-494f-86e3-be93347c4ac2
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 239ecca5-7a4f-4130-a94a-91df764a2bb5
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: e959a077-d214-4c00-9c9d-25ff1ffa256a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 0e94082f-30e1-4811-81e1-f1472d6ee5bb
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: fe63bbb4-668d-4ddf-884b-00a98d6af572
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 8cd6ca40-bd37-4dd7-b04e-856f17bfca97
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 783e4f87-80bc-440f-84a8-d64a60435548
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 048a3fe6-29f3-4844-b8bf-a19f7ac3798a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 573bb745-a6a8-42f6-999c-77fc43610717
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: ddfa4470-f6e1-48d5-8970-811c65d16977
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: ee1b1e28-98c2-45d8-83a0-61cc14566321
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 41797730-cdbc-4b8c-b3a0-f6688301b2d9
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: fc35551d-b99e-42ab-9eca-4de71e217a15
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 4aa2d06d-5c54-48f4-85c6-182fdf9bc9e4
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 851ee792-6b98-4256-9487-9a3ecae5eeff
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: ff7a458f-61d2-484b-a042-e27cfeeb15d8
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: ed4dd644-d955-4df7-a6e6-474fb82097ac
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: cb5fe7de-f933-433d-8075-93eb003ab0cb
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: bc63cfee-5f48-4075-9b78-4044451159a9
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: c5505796-4879-4567-b1f9-cbd70a7a46f6
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 99dfd501-15c9-4463-acdc-1967ec6bb841
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: dc1ba531-1308-4468-ac02-34255738f81f
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 63511d1a-1b93-43d9-a179-4c6a6a49ff91
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 86e233d7-1886-4382-b1c4-812b94b45516
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 036e021d-c023-4ae4-9526-61b457dc232a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: e1c7e648-bcef-4df2-9acf-138cc3b1cf0a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 2e716b34-41a8-415c-9557-abd2da0576c4
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: ae8fc72e-f5fa-4915-8afa-4fbdba54a503
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: d37f6b3a-4b51-4657-b490-26bd7a861236
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: abf57f6c-427c-474f-9e91-c6d40993783d
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 1d673197-b67b-489c-abb9-efba31dbfb4d
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: c00978fc-dcaf-4abd-aa98-0971bc7f4205
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 9926a651-8473-44b2-9d43-dc7faee3bdfa
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: e0152fb1-aa5a-49f7-bb6e-477964999f4c
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32e64aa9-98f1-4ad4-970f-d37924db0791
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24a47dab-b5a3-465a-bc69-ddf9e8a20334
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b059b73-2321-4996-8286-8f347da1913c
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 31bf6dec-4a20-4452-9034-5b98730fd580
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: e6946abb-1ba1-4661-9e7e-c35ffe303ab2
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 8d7af509-6180-4efe-bd3a-8199e9cd8d9a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 444285b1-28c7-4be9-a929-b8ae1966df61
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 17f891a7-5af9-4734-826f-93109bb8dd36
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: d43dad3c-e24a-4e1b-83bc-2a0a430f7582
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 2863828c-43e1-43a8-b18e-fcc0e23e396e
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: d196c09b-3fc5-46a5-b18a-e8cbe25cf04a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 72984539-13e7-4be8-b670-53785f5cb17a
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: c03e92e4-f728-4ff5-b891-a4dd125bc64d
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 39672a96-1bb3-433e-9ae1-8872ec34a5d7
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 03f612ba-88cd-4d96-8e16-a6a12f3accc3
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 5d17afc8-7e23-4cfa-a2c1-a4e88c2df594
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: c6e88ed7-f740-467b-a47a-462974b65f7d
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 488dbb1e-c10c-4036-b53d-9f9c8ab955c1
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb72c06c-998b-4a19-9167-bc0f2d5dad49
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e8b485c-4975-47b0-b6d7-dd4a2498ed6e
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df3a1790-39f4-4d6a-9f17-ca6ff9e4c39d
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 8e5a61e5-5674-4185-8e09-0cc3a401e5d7
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 5d2d7f02-fc75-43ca-bc68-94f5d9a2d5ee
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 30bc032b-85e4-4207-a853-b11550fa6cd8
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 9228165a-8e73-489f-957a-149753f1b904
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: b33f134a-1416-44ed-965f-1b5107181ce8
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 2d8628a5-b93a-407b-b0fb-985aa4f76b8e
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: a0866262-52a2-4a4e-85d1-bac47dc20622
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 26651f63-ee8b-472e-b939-1553f34d459b
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: 9661a5a1-558f-453c-b4ec-a00f800ed299
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 09649df1-718b-4b05-bf66-51f89eac8ec2
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: 963f0949-7907-48af-932b-e05c590029a5
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    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: b8429a22-dd9c-4127-aec3-4652a09a3d7c
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9bb9da3-82d8-4136-a7bb-362fab5d8a6c
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43de7660-ea03-4376-a041-3d36890fb3cb
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddc3a4f4-ef18-4436-aad0-a3bf3f92be84
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 854
    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: 78d90d59-78b3-42d7-b1d1-a64f6d690687
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 856
    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: c348934b-f943-41ac-a874-a001d0d7bde7
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p0_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e02b4e2f-953c-436e-97ae-5700410968c2
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      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: 73e17a41-aa29-44d5-aabb-ed7dae848e46
    creation_time: 2024-07-04T11:36:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/safe001_power.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe001_power.oepc.i: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
      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/safe001_power.oepc.i
    file_hash: 67d3e2c6779f32015be5c9fe966e6a739e1c762dcde7f287ad383839eb490e84
    line: 852
    column: 3
    function: main
