- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4595bbb7-4f0f-4522-bd24-769cba296d6d
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99a392f0-1c1a-4735-b417-5b9383f9e968
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75351435-16fd-4f9e-9765-3e8c52fa3208
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c7878d8-cbd0-44f6-ad2a-9765eaed847b
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7b18f69-4d21-4422-be81-b40423a59115
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f7eb366-e0dc-458f-ac33-f2917e517fe9
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c7629d3-4ef4-4e86-abd8-919302423829
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b9c06df-4bf0-45ba-9469-4d9344834931
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0900b8c1-a028-4859-8ca5-27948e682bf7
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX)
      && 0 <= a) && 0 <= b) && 0 <= b$mem_tmp) && 0 <= b$w_buff0) && 0 <= b$w_buff1)
      && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX
      <= 1) && __unbuffered_p3_EBX <= 1) && a <= 1) && b <= 1) && b$mem_tmp <= 1)
      && b$w_buff0 <= 1) && b$w_buff1 <= 1) && x <= 2) && y <= 1) && z <= 2) && b$flush_delayed
      == (_Bool)0) && b$r_buff0_thd0 == (_Bool)0) && b$r_buff0_thd2 == (_Bool)0) &&
      b$r_buff0_thd3 == (_Bool)0) && b$r_buff0_thd4 == (_Bool)0) && b$r_buff1_thd0
      == (_Bool)0) && b$r_buff1_thd2 == (_Bool)0) && b$r_buff1_thd3 == (_Bool)0) &&
      b$r_buff1_thd4 == (_Bool)0) && b$read_delayed == (_Bool)0) && b$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p3_EAX
      == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (b == 0 || b == 1)) && (b$mem_tmp == 0 || b$mem_tmp
      == 1)) && (b$w_buff0 == 0 || b$w_buff0 == 1)) && (b$w_buff1 == 0 || b$w_buff1
      == 1)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((z == 0
      || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fda53464-5eab-4ccf-aa3b-be4804440eca
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX)
      && 0 <= a) && 0 <= b) && 0 <= b$mem_tmp) && 0 <= b$w_buff0) && 0 <= b$w_buff1)
      && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX
      <= 1) && __unbuffered_p3_EBX <= 1) && a <= 1) && b <= 1) && b$mem_tmp <= 1)
      && b$w_buff0 <= 1) && b$w_buff1 <= 1) && x <= 2) && y <= 1) && z <= 2) && b$flush_delayed
      == (_Bool)0) && b$r_buff0_thd0 == (_Bool)0) && b$r_buff0_thd2 == (_Bool)0) &&
      b$r_buff0_thd3 == (_Bool)0) && b$r_buff0_thd4 == (_Bool)0) && b$r_buff1_thd0
      == (_Bool)0) && b$r_buff1_thd2 == (_Bool)0) && b$r_buff1_thd3 == (_Bool)0) &&
      b$r_buff1_thd4 == (_Bool)0) && b$read_delayed == (_Bool)0) && b$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p3_EAX
      == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (b == 0 || b == 1)) && (b$mem_tmp == 0 || b$mem_tmp
      == 1)) && (b$w_buff0 == 0 || b$w_buff0 == 1)) && (b$w_buff1 == 0 || b$w_buff1
      == 1)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((z == 0
      || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa840dfb-5bd0-429d-aa26-2ad590d837a2
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX)
      && 0 <= a) && 0 <= b) && 0 <= b$mem_tmp) && 0 <= b$w_buff0) && 0 <= b$w_buff1)
      && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX
      <= 1) && __unbuffered_p3_EBX <= 1) && a <= 1) && b <= 1) && b$mem_tmp <= 1)
      && b$w_buff0 <= 1) && b$w_buff1 <= 1) && x <= 2) && y <= 1) && z <= 2) && b$flush_delayed
      == (_Bool)0) && b$r_buff0_thd0 == (_Bool)0) && b$r_buff0_thd2 == (_Bool)0) &&
      b$r_buff0_thd3 == (_Bool)0) && b$r_buff0_thd4 == (_Bool)0) && b$r_buff1_thd0
      == (_Bool)0) && b$r_buff1_thd2 == (_Bool)0) && b$r_buff1_thd3 == (_Bool)0) &&
      b$r_buff1_thd4 == (_Bool)0) && b$read_delayed == (_Bool)0) && b$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p3_EAX
      == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (b == 0 || b == 1)) && (b$mem_tmp == 0 || b$mem_tmp
      == 1)) && (b$w_buff0 == 0 || b$w_buff0 == 1)) && (b$w_buff1 == 0 || b$w_buff1
      == 1)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((z == 0
      || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2aab14c-cec2-40a2-b304-531eee1bfbeb
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX)
      && 0 <= a) && 0 <= b) && 0 <= b$mem_tmp) && 0 <= b$w_buff0) && 0 <= b$w_buff1)
      && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX
      <= 1) && __unbuffered_p3_EBX <= 1) && a <= 1) && b <= 1) && b$mem_tmp <= 1)
      && b$w_buff0 <= 1) && b$w_buff1 <= 1) && x <= 2) && y <= 1) && z <= 2) && b$flush_delayed
      == (_Bool)0) && b$r_buff0_thd0 == (_Bool)0) && b$r_buff0_thd2 == (_Bool)0) &&
      b$r_buff0_thd3 == (_Bool)0) && b$r_buff0_thd4 == (_Bool)0) && b$r_buff1_thd0
      == (_Bool)0) && b$r_buff1_thd2 == (_Bool)0) && b$r_buff1_thd3 == (_Bool)0) &&
      b$r_buff1_thd4 == (_Bool)0) && b$read_delayed == (_Bool)0) && b$read_delayed_var
      == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p3_EAX
      == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (b == 0 || b == 1)) && (b$mem_tmp == 0 || b$mem_tmp
      == 1)) && (b$w_buff0 == 0 || b$w_buff0 == 1)) && (b$w_buff1 == 0 || b$w_buff1
      == 1)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((z == 0
      || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b8dc82f-9343-4a02-b366-4f235c8b7a6b
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e5e2a3d-b203-4e74-8db1-2e41bc47bb4c
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ea943e3-cb88-4da1-95cb-bfbd8f15310a
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cba8ac78-f355-40a1-9bdf-5fd55e63db19
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0486376-65ea-4f94-af8f-c23ca57b387a
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff1 && b$w_buff1 <= 1) && (b$w_buff1
      == 0 || b$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6418acae-f9a5-4cdf-bca6-542e07955917
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff1 && b$w_buff1 <= 1) && (b$w_buff1
      == 0 || b$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 178881d0-d8b8-48df-befc-909baad26f8d
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff1 && b$w_buff1 <= 1) && (b$w_buff1
      == 0 || b$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f6b5d73-ff52-459c-8a57-2bfa3f9763b3
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff1 && b$w_buff1 <= 1) && (b$w_buff1
      == 0 || b$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6f247b8-07ef-49bd-a807-47ebcf03c159
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 188f1cc5-047d-4300-9a1a-80647038f900
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfc4ebe4-1626-4131-a36a-3dab7dde2a91
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5207d79e-abef-44c9-9f5f-f50603e0a572
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1755c39-3a85-4742-a58a-e736b9d85af7
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af369a8c-37e6-411e-abcb-1251e740374a
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e5c1116-e69d-4564-95e7-4e8a66aacae9
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69a22879-f406-4348-9394-3f3fbffb8fea
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a199287-be91-43a5-9dbd-7a6771d20095
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4519782e-e08f-415e-b3a8-80610ac86c90
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ade975a-75af-4bd2-a191-b025ca7eb26c
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16ea2d53-3e89-4a35-ba3f-2d049b162441
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48d9c212-618e-4223-a000-1ec457877c67
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9eae295d-b94e-4699-a65e-44f2111e7150
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5f11dde-c481-474d-831e-87a9c05a0ae4
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e20a6d77-53fd-427e-876a-77816159b301
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23c7d0ae-157e-4365-8640-c22e79f15714
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3c84e2a-d0cb-4bc1-bf25-d8bba5d7df84
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97e32ec0-cdc9-4153-95f5-cd52bf195c42
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7802234-6dbb-4d08-b377-c906d01600a7
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1696a23-d2ad-4925-8b6d-02bf284f0951
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44c2a439-801c-4e39-84e5-ada734f627ce
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8ebdb69-055a-43d6-ad54-ab6bdbd869ba
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9eede7f6-29dd-4a5d-8bd0-e98c7d5f1f0d
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72337eed-9c7d-4a4a-882c-0e4c07ecca0f
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5534ec9c-45a4-4a80-818b-42c0372421b4
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3b19b17-bd67-41a0-a13c-25b3ce5b6e2a
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 301862fb-d722-479f-84c0-de6c5e9fec48
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e97e5f7-bba7-4a47-b32b-3288fa823660
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$mem_tmp && b$mem_tmp <= 1) && (b$mem_tmp
      == 0 || b$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f69d266e-bbb1-444f-a01f-abaf8f03e6bf
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$mem_tmp && b$mem_tmp <= 1) && (b$mem_tmp
      == 0 || b$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed8d8a9c-a039-40fe-be13-4765fc2465ae
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$mem_tmp && b$mem_tmp <= 1) && (b$mem_tmp
      == 0 || b$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88797684-069a-4fbc-b5b2-a62ab491d488
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$mem_tmp && b$mem_tmp <= 1) && (b$mem_tmp
      == 0 || b$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6676c819-32b8-4252-86a2-1548711bd79c
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2516d9a0-1dbc-46bb-a42c-ce0d9cb7e018
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b360301-c1c2-4a4f-968c-91caa891a607
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a993abde-3aa4-49bc-ace7-bfa826976f9f
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3df41976-d32e-411c-812c-7cc94b6b94b0
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e60b69f-36de-4334-8043-bf638102a9de
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05a11746-4eeb-47b6-97f2-96be00b536ba
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e033d817-d280-4dfe-a948-ee43275139fc
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1b6bd07-f2b4-4b60-bbe0-6df81b95ba68
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c957545-34e5-46bf-b74e-eb20e4e412d5
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 001986c8-fab3-411c-b686-d558e00da5d4
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a27116e-926e-45f0-b9d8-f37cb4da321e
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cdf467c0-bed3-4aef-bc7a-b9bb8e4ebb19
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bef039ec-f49a-4b5b-a45e-12c0f17fea2e
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb8f9083-f161-44b1-98d9-740e070577bb
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de5cd902-69a4-4b61-b860-61829a56a494
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59356886-4f64-47fc-923d-738807d8f9be
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4753857-75fc-482b-9d85-05add9a8b06e
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1252cdde-c6e8-40aa-b407-c240a20af68a
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fd009d0-e2ee-4769-97d5-08447aa7645a
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bc4b149-c475-4227-9c40-4de8bd5915dc
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80d42a9e-578d-4109-92ef-79b0406f396f
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aebb3ec5-c7d6-4272-8128-5878f24dbd25
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdb30479-340c-4448-95f0-b5da135467f3
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 685f4bf3-4668-4c27-8425-fb87f9413ed1
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec1ac420-c26b-418d-90bc-6373dc0db935
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2db7187a-2d56-4fc6-aa24-d7abdaa39452
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c111f05-248f-4f93-9495-008bf65196ff
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1e4af09-313b-4aea-bf4c-dc1f02012b61
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    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: d7779a8b-7aed-4229-b83c-ce9992c0ba9e
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    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: 00c4fe33-423a-4b55-831c-716e9fa2ff53
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    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: a895f83c-df39-4b49-ad02-b9797abd7fb8
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    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: 450a77cb-0ea6-4a7a-b11c-d0696546cc49
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff0 && b$w_buff0 <= 1) && (b$w_buff0
      == 0 || b$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a0ec640-d9f5-4277-a04c-e705884e3a1c
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff0 && b$w_buff0 <= 1) && (b$w_buff0
      == 0 || b$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ab3105c-19bc-4e4b-bf21-f1c2603085f5
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff0 && b$w_buff0 <= 1) && (b$w_buff0
      == 0 || b$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cc0aabc-be02-43b0-b79f-e8c83510d463
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b$w_buff0 && b$w_buff0 <= 1) && (b$w_buff0
      == 0 || b$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2b94b28-866a-41b8-9bfe-9dd1f87e2dd5
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 872
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 380b9a1d-c34e-4e0f-8604-1108dd5c11cd
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3c9e34f-2e06-4464-bea4-a6191322ed64
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c02ecb56-3f01-4435-b226-d2954ee82be9
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 877
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 0694b9dc-2dfe-4991-a755-8acdb3b165ff
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      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: 9cb9f4c2-02e5-4910-a6db-73183f8bb389
    creation_time: 2024-06-18T14:55:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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/mix044_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix044_power.oepc_pso.oepc_rmo.oepc.i: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
      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/mix044_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: 40f0a1ff0b59c9897722e1cc89a9065b61569e5c28581990c7adb84261d57e0b
    line: 870
    column: 3
    function: main
