- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bd27a0e-31b3-4b32-9024-8d5902c3553c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: 96d0b321-695e-4263-8895-479d7efd5cf6
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: b5f4ef90-91cd-47c2-b8c1-4e886f6ad03e
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: b935d445-9a11-4fe7-a237-38e043963d16
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31c9066b-f1fa-4c42-8d00-cc07aef621b9
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fdabbcc-4a7b-48f2-bb5e-7a94051e6946
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9714bda6-ed6c-4859-af5a-678aa5912d04
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0)
      && 0 <= y$w_buff1) && 0 <= z) && x <= 2) && y <= 0) && y <= 2) && y$mem_tmp
      <= 0) && y$mem_tmp <= 2) && y$w_buff0 <= 0) && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff1 <= 0) && y$w_buff1 <= 2) && y$w_buff1 <= 127) && z <= 2)
      && z <= 127) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd2 == (_Bool)0) &&
      y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && y$w_buff0 % 2 ==
      0) && y$w_buff1 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2)) && (y$w_buff1
      == 0 || y$w_buff1 == 2)) && ((x == 0 || x == 1) || x == 2)) && ((y == 0 || y
      == 1) || y == 2)) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))
      && ((z == 0 || z == 1) || z == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fd565e7-ad33-4497-b6a7-69c199353ac1
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0)
      && 0 <= y$w_buff1) && 0 <= z) && x <= 2) && y <= 0) && y <= 2) && y$mem_tmp
      <= 0) && y$mem_tmp <= 2) && y$w_buff0 <= 0) && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff1 <= 0) && y$w_buff1 <= 2) && y$w_buff1 <= 127) && z <= 2)
      && z <= 127) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd2 == (_Bool)0) &&
      y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && y$w_buff0 % 2 ==
      0) && y$w_buff1 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2)) && (y$w_buff1
      == 0 || y$w_buff1 == 2)) && ((x == 0 || x == 1) || x == 2)) && ((y == 0 || y
      == 1) || y == 2)) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))
      && ((z == 0 || z == 1) || z == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0563f888-e2e2-4e97-8f84-b258368e76a4
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0)
      && 0 <= y$w_buff1) && 0 <= z) && x <= 2) && y <= 0) && y <= 2) && y$mem_tmp
      <= 0) && y$mem_tmp <= 2) && y$w_buff0 <= 0) && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff1 <= 0) && y$w_buff1 <= 2) && y$w_buff1 <= 127) && z <= 2)
      && z <= 127) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd2 == (_Bool)0) &&
      y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && y$w_buff0 % 2 ==
      0) && y$w_buff1 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2)) && (y$w_buff1
      == 0 || y$w_buff1 == 2)) && ((x == 0 || x == 1) || x == 2)) && ((y == 0 || y
      == 1) || y == 2)) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))
      && ((z == 0 || z == 1) || z == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35c72257-64c6-4021-af09-49e262d6a86c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 2) && ((y == 0 || y == 1) || y ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c10fc59-27f9-42ba-ad3b-a341ab9f32cd
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 2) && ((y == 0 || y == 1) || y ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 908b2ba2-0b6f-4e06-996f-0835613dee41
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 2) && ((y == 0 || y == 1) || y ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef16c7b7-7d1b-4f0d-8083-b4f7d864ce9b
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: cdf8fd1a-6733-44c5-8c6f-821d17d48dd8
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: e6f6ec57-fd09-457e-811a-1b8fc848934c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: a06da29a-b81d-4f9b-8e64-9239b73f171c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: 3647f8d4-5a77-4048-8e86-733e41c1bdf1
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: bbe1894a-7998-4bf0-ad65-d691149a6965
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: 77176bdc-c4fa-4e43-b525-85e41cea219a
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: edfe7654-dbe0-4caa-93eb-e522a61085bb
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b99f743d-5bb3-4c8d-9406-53647df13035
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff0 && y$w_buff0 <= 2) && y$w_buff0
      <= 127) && y$w_buff0 % 2 == 0) && (y$w_buff0 == 0 || y$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a5cf0f0-949b-4646-bcf4-c0f50f327784
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: a0a7b2f3-5267-43de-b9c9-7f75e7b02c83
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: a7087a63-5fa5-4457-acfc-4cdc3e3b65b0
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: 2c5e498f-7e9e-409f-ab34-7d573c5983f5
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: 04916a32-fc80-4fd2-bdf5-fb39b42ebaf2
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: 3e291256-5892-46d9-9bbf-45bbbd927299
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: 6c7c7d5e-b767-403f-951b-0f7f3582a201
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: 286696ff-204b-41d9-81b8-3d7ade19ed4c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: 9d9a317a-cd74-4bbc-8a84-2a49193706d9
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: 5daf8f76-392a-4e32-a46a-84c8da8dd9f7
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: 3595b03f-ec1d-4fb9-a302-d43273ed72e9
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: 474ff531-bead-49ae-a34c-53cfcf772e42
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: 24412b66-cfe4-4a20-8981-e7a902c0aab8
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: 530a5f91-c53b-4240-bd1d-98a7f778e78e
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: 19ab4524-19d0-4b04-b602-f20fc183d30e
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: 1b6a2392-ab10-4a42-bc2f-26651eb375cd
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1821db7a-ed42-4113-8aac-6373c0669e0c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f165319d-065d-4f66-9ed9-bc2882d580d1
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y$w_buff1 && y$w_buff1 <= 2) && y$w_buff1
      <= 127) && y$w_buff1 % 2 == 0) && (y$w_buff1 == 0 || y$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54a8351b-6276-433f-bc88-22905f01a64f
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 2) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a537ad2-d7d3-4f4a-bc4a-668436cfc2d0
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 2) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 273ec282-e46f-4144-9083-54cddc7fe1b8
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 2) && ((y$mem_tmp
      == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3a32343-5641-4c3a-adae-e473a213c607
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    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: bd1c884d-df88-4439-b43a-96f27bdb9e02
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    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: d34d916c-3516-49c1-b987-4406dc7ccf3a
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    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: d9dbbbdc-6d71-4b79-b17f-0ef47f9b85ee
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 814
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aefa016b-6c4a-41f1-96d9-c5500bea4945
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 816
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d73a55be-e9d2-49de-9d13-96bda1073aaa
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f6d92765-9166-4959-9602-a59a6e4b0faf
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bc6d9847-23e5-4fb6-83b8-4578bc6b764d
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 743
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ef8d98b6-b38f-4d30-97b8-d708b6ddc650
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 784
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 48e9651c-9196-49ea-9797-b74fb6a986a9
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 827
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cffc0a24-a3ae-4624-b9ab-29d594c243f7
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 756
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 64263b6a-fae2-4fb0-948d-5587c3c153fb
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 795
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 389e5eb9-7acc-466e-a093-3b7a06035a65
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 788
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f11b8da7-ac12-49b3-bb60-e790926fabc0
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 753
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a30270c1-05ad-4b19-91ea-817a449bdf87
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 755
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e327f379-570f-483f-a446-c9af11bc9f77
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 787
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f0f4aca5-343a-4cda-94db-28159ebb7968
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 819
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c719c4f4-1839-4edd-93f8-b4867b2866a5
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 746
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 06265753-5f52-4225-a8b0-f4a4b483be0e
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      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: 3d521c3d-1273-4293-95c9-0530ce3166dd
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 812
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6c0415ed-d130-4b92-ab05-bf25c11c382c
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 817
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 22c5996a-367d-401e-b3c7-b950a26699b6
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 758
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fc7003a6-0cd2-45a2-a7a7-1c5dd0be804d
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 80aeeb09-841a-44aa-803c-0af79905aca1
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 744
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5742966c-24ec-4f9b-99e6-71cb7b3dffb0
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 843
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b7bfb9c0-7f44-4fbf-8e27-6fb6cf35dd97
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 785
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 91fb5b66-9bcf-4ab0-80ed-a1bdeb7e3cb6
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 821
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d5214fc7-bffc-4af7-97c9-0781a822f5a7
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 773
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 977147ed-87d5-477e-956a-aef3e0c75260
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 768
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 732bd7a2-7fee-4e0e-a981-68edd2515140
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 740
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 65a4475b-01a9-49c8-9606-69b43d55de47
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 741
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2313abd2-159a-4b91-b955-b057163538c6
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 828
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5ab481e2-a775-4db0-8fca-3a160968a96e
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 745
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f25a7aae-b973-4e86-ba88-1f231e94d9fe
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 738
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 73f5fd16-e9fe-4fb7-8bf6-f62cbd90c263
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 759
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 591600a2-3f38-48ed-8a0a-867591c40042
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 765
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5bd66ea8-fcfd-48b6-abf6-0e63dfcb39cd
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 766
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e8127961-d72c-47b9-a1ac-f451c3d2d0da
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 797
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 256ff9c9-ced7-40ca-8694-f6a616b94700
    creation_time: 2024-04-29T11:51:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe030_power.opt_pso.opt_rmo.opt.i
    file_hash: 6e0191a7c0154db5e6d5798f5b20e5814ce0ff555e18a7acf1f1e5e323a36576
    line: 794
    column: 3
    function: P2
