- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e195b31-a48b-46ff-837b-c53dd126734f
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 475e40c5-caae-444c-97bf-655412f4fde4
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10cc9d5a-f354-41a6-86ba-ceddeacf5786
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a46762f-b615-4e63-8f26-7f11c9f60aa7
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90affde4-8479-49f7-82fa-3ab11ec8dd05
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((((((((((((((((((0 <= __unbuffered_cnt && a$flush_delayed
      == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0) && a$r_buff0_thd2 == (_Bool)0) &&
      a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4 == (_Bool)0) && a$r_buff1_thd0
      == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) && a$r_buff1_thd3 == (_Bool)0) &&
      a$r_buff1_thd4 == (_Bool)0) && a$read_delayed == (_Bool)0) && a$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p2_EAX
      == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0
      == 0 || a$w_buff0 == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 ||
      y == 1)) && (z == 0 || z == 1)) && ((x == 0 || x == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7acba7d-2e8f-45e9-aa02-1c722968caa6
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((((((((((((((((((0 <= __unbuffered_cnt && a$flush_delayed
      == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0) && a$r_buff0_thd2 == (_Bool)0) &&
      a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4 == (_Bool)0) && a$r_buff1_thd0
      == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) && a$r_buff1_thd3 == (_Bool)0) &&
      a$r_buff1_thd4 == (_Bool)0) && a$read_delayed == (_Bool)0) && a$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p2_EAX
      == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0
      == 0 || a$w_buff0 == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 ||
      y == 1)) && (z == 0 || z == 1)) && ((x == 0 || x == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2355fb13-a8c3-4009-9963-1e274b83afbb
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((((((((((((((((((0 <= __unbuffered_cnt && a$flush_delayed
      == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0) && a$r_buff0_thd2 == (_Bool)0) &&
      a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4 == (_Bool)0) && a$r_buff1_thd0
      == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) && a$r_buff1_thd3 == (_Bool)0) &&
      a$r_buff1_thd4 == (_Bool)0) && a$read_delayed == (_Bool)0) && a$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p2_EAX
      == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0
      == 0 || a$w_buff0 == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 ||
      y == 1)) && (z == 0 || z == 1)) && ((x == 0 || x == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21bae8a0-de93-4773-8fe9-0c4e2e6d1e72
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((((((((((((((((((0 <= __unbuffered_cnt && a$flush_delayed
      == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0) && a$r_buff0_thd2 == (_Bool)0) &&
      a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4 == (_Bool)0) && a$r_buff1_thd0
      == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) && a$r_buff1_thd3 == (_Bool)0) &&
      a$r_buff1_thd4 == (_Bool)0) && a$read_delayed == (_Bool)0) && a$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p2_EAX
      == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0
      == 0 || a$w_buff0 == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 ||
      y == 1)) && (z == 0 || z == 1)) && ((x == 0 || x == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfb937c6-e165-470c-8aa9-050c833846ae
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0828c01-7ad5-473a-8047-1a9268b9c23c
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 451dce50-32a3-48a6-a84a-18060c0798ea
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b1fa019-5146-467b-89aa-540fd442e478
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1705c9fa-1faa-415a-b867-295e75122630
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$mem_tmp == 0 || a$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af87df73-ad3d-4245-be99-6240d4dca0b4
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$mem_tmp == 0 || a$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6b8a90f-704d-4d2a-a608-e52572fc132a
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$mem_tmp == 0 || a$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd5d2de8-0706-4ef7-aa74-10f265e2626e
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$mem_tmp == 0 || a$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aae9afc4-4b5d-484c-8235-bf127480e3b2
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d53f4d5e-c763-4b1e-bfb4-64b3f5d7c58f
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15332ed2-e35c-4b6e-b009-b79e959663e7
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eee99c7c-6945-4a7c-bc56-43521c9b8b82
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a370db8-327f-4449-adb7-67b2709e01af
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f476139-90d0-439a-9652-1e0781177750
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a88d9eb4-3af6-4343-a1f6-b16b0902f6ec
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9b758bf-5ff7-48a4-932e-8d6e2977d725
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b17647f-e06b-432c-b97d-bfc5dd934d4a
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ba0ef07-5aea-40b5-9171-2aa4c83f6e46
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53e03989-3f13-429a-aea7-8f441d4a17df
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b598a127-93be-4986-86c5-8f9ac69ef533
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 459081fb-5402-45b5-a3ee-5afaeb893799
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb1ff4c8-9bb5-4a35-8969-ae3cc423d710
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce0fdad4-80a9-4fe1-8f36-af7e995a5360
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd8124c5-d26e-4566-8e11-5274e2c8b177
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b58d8f8b-700a-4a1a-9892-31a628a7b46d
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c36c3b5a-d397-4a7a-ab89-7000cf917eb3
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebebfff8-ef78-4ea8-b883-8f1518d2cb11
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0b0ea71-0060-49f8-9418-750a4742970e
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eab0ace5-69c4-4191-a0f2-d390ffeefcdf
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b40da55-c137-4252-a37a-feaa2e9c76c1
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f10d3d8-204e-4b10-8036-9aa158d0925c
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbfdffac-c13d-49fe-9dc1-f26975fa2d68
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77d358b0-87b5-4c29-a859-27d447b3e428
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9921a183-3194-4a57-a937-0f5bb2cf50a7
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64905fc9-831b-4746-b07b-16f3d49c3977
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b96d1831-b1e4-4b6b-9a53-69f6a2a55d9c
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f2ea1b6-e36a-4147-86aa-be24052c120c
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75484ef2-ed78-4360-9145-cd08dac43987
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea1803f4-d3b8-4ea2-81a0-2a48a0696556
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ded93b8e-8b65-4a04-8b24-68da36fe4c92
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbe7bcb8-5197-4e0c-bbfe-19f3a9b27096
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a587f38e-8e66-4841-9ce7-7e13ac3984ff
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e9a1aef-efde-44a6-9fa5-5daa1fb9466d
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77df8d1b-d003-472f-9b47-a0388d800403
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bea86280-4a97-4437-a70b-c8fe52faa247
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7e64da0-5d57-49ec-8a06-7cf9f8040cae
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbff7017-99a1-431e-a9a5-00eea0bf4546
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bac4a35b-6b5e-4fd2-8f38-2572ecaa1eb8
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4474239-8893-4757-b635-acac7f22e9a6
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d864762-b346-46bd-b870-2e70e709afe3
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbdc8f41-34c8-4081-af6e-ff1442c657e5
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 622f0986-38e5-4fb1-a45b-71d8b02e5b8f
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7351285-8ed7-4066-b080-2023513a82a0
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99e0e7b7-b482-4504-be11-bc7658deb459
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a97fcf4-1746-435b-83cf-3384c22caf82
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a64fddcf-d0de-4786-bebe-0eb3c328262f
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ecabc8f-3ae7-492a-ab3b-4476670433f0
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ee5c380-c8aa-4390-a8dd-e5adfc3022f7
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd53ab0b-a170-445a-afc7-fcd76ccb3409
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64e8f5c3-687b-4a03-8cea-2eb690de72ff
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0df3603-4b43-4d95-9b88-74c2b63d2ca6
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff0 == 0 || a$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a5f06f7-83a5-4165-973f-de9500d5fca8
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff0 == 0 || a$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 985e5f27-03a2-4032-ae96-5807ec72baf6
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff0 == 0 || a$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e825f7e3-739b-45fe-a348-cbb82e202e9d
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff0 == 0 || a$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2d7e3ba-082e-4426-a3b2-2cbd1fdb8ac6
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5a0a549-003c-461d-bd38-af97ac5b6013
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 304f36cc-b015-4b9c-8b09-524c4c9defe5
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba705805-9aed-4536-bcbf-e9d7a6e2d1f0
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 408e3f31-270a-4aab-a9e0-87db92893de3
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    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: a44ab701-c767-4830-a53b-98cab596e637
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    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: ab85da90-405f-46bf-90f2-5cd1420b361f
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    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: 83a6f1ba-ebe8-49e1-b188-b0f7eeeccb52
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    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: cc725b2f-d3db-483a-92f0-f32b0a274af5
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff1 == 0 || a$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7244f3e1-73fa-412a-a430-4653ab5c909d
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff1 == 0 || a$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca16b139-02db-4f20-8d70-d5520fa80430
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff1 == 0 || a$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecba525c-53e5-4938-ab79-94e05a73537c
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a$w_buff1 == 0 || a$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89d86eed-8516-4993-b478-0e409fb83456
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 696e6a54-5707-4553-85f5-3a3fd54de3d4
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6dc34feb-0c49-4957-9592-c50197d606fb
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 868
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97835896-6bfd-47a0-9b54-82eac2cf858e
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 4ee8a5cf-dd18-415b-b53d-73e7256c4e47
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      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: aeb54877-fbb1-4013-8a46-4216bc9f0f7a
    creation_time: 2024-06-19T11:47:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
      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/mix051_power.oepc_power.opt_pso.oepc_rmo.oepc.i
    file_hash: 76dbb78f4fe406633111c7d7e2c1e8bd933a1f67e6e1cf5d4cbd1b0379bfe086
    line: 862
    column: 3
    function: main
