- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d82e918-f6b8-44b3-aeb9-c87730394d19
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p1_EBX) && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX)
      && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0) && 0
      <= z$w_buff1) && __unbuffered_cnt <= 0) && __unbuffered_p0_EAX <= 0) && __unbuffered_p0_EAX
      <= 1) && __unbuffered_p1_EAX <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX
      <= 0) && __unbuffered_p1_EBX <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 1) && __unbuffered_p2_EBX <= 0) && __unbuffered_p2_EBX <= 1) && x <= 0) &&
      x <= 1) && y <= 0) && y <= 1) && z <= 0) && z <= 1) && z$mem_tmp <= 0) && z$mem_tmp
      <= 1) && z$w_buff0 <= 1) && z$w_buff1 <= 1) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff0_thd3
      == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) &&
      z$r_buff1_thd3 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EBX
      == 0 || __unbuffered_p2_EBX == 1)) && (x == 0 || x == 1)) && (y == 0 || y ==
      1)) && (z == 0 || z == 1)) && (z$mem_tmp == 0 || z$mem_tmp == 1)) && (z$w_buff0
      == 0 || z$w_buff0 == 1)) && (z$w_buff1 == 0 || z$w_buff1 == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cba90e8-80f4-4c4f-b596-0aac91de9bd4
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p1_EBX) && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX)
      && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0) && 0
      <= z$w_buff1) && __unbuffered_cnt <= 0) && __unbuffered_p0_EAX <= 0) && __unbuffered_p0_EAX
      <= 1) && __unbuffered_p1_EAX <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX
      <= 0) && __unbuffered_p1_EBX <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 1) && __unbuffered_p2_EBX <= 0) && __unbuffered_p2_EBX <= 1) && x <= 0) &&
      x <= 1) && y <= 0) && y <= 1) && z <= 0) && z <= 1) && z$mem_tmp <= 0) && z$mem_tmp
      <= 1) && z$w_buff0 <= 1) && z$w_buff1 <= 1) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff0_thd3
      == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) &&
      z$r_buff1_thd3 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EBX
      == 0 || __unbuffered_p2_EBX == 1)) && (x == 0 || x == 1)) && (y == 0 || y ==
      1)) && (z == 0 || z == 1)) && (z$mem_tmp == 0 || z$mem_tmp == 1)) && (z$w_buff0
      == 0 || z$w_buff0 == 1)) && (z$w_buff1 == 0 || z$w_buff1 == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7d66269-31b3-4021-aea1-c90e39cf3c94
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p1_EBX) && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX)
      && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0) && 0
      <= z$w_buff1) && __unbuffered_cnt <= 0) && __unbuffered_p0_EAX <= 0) && __unbuffered_p0_EAX
      <= 1) && __unbuffered_p1_EAX <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX
      <= 0) && __unbuffered_p1_EBX <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 1) && __unbuffered_p2_EBX <= 0) && __unbuffered_p2_EBX <= 1) && x <= 0) &&
      x <= 1) && y <= 0) && y <= 1) && z <= 0) && z <= 1) && z$mem_tmp <= 0) && z$mem_tmp
      <= 1) && z$w_buff0 <= 1) && z$w_buff1 <= 1) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff0_thd3
      == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) &&
      z$r_buff1_thd3 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EBX
      == 0 || __unbuffered_p2_EBX == 1)) && (x == 0 || x == 1)) && (y == 0 || y ==
      1)) && (z == 0 || z == 1)) && (z$mem_tmp == 0 || z$mem_tmp == 1)) && (z$w_buff0
      == 0 || z$w_buff0 == 1)) && (z$w_buff1 == 0 || z$w_buff1 == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b265fa02-c87f-48dc-9b4b-d8fb4963948c
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65ce6ada-5be8-4d6b-ab8c-146a1109e6c8
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 66d7b9fd-e37a-4e74-b1ac-affe9aa5e193
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5810b20d-4c73-4878-808f-286ddf96e573
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89a93d77-19a0-42c5-aadb-e512a1ec59c0
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb8cd0a2-fefb-4535-afa7-be03fe9d835f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fa2cbaa-3399-4208-88d5-f8b02107847f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adc02ad3-1fda-4d48-8ac4-66c0290cfb3f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 824b1680-cd72-4ba1-9d9d-43d7dce84fb4
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 264e963e-91a6-4a62-8de2-7d212107fab3
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 994a4b02-dbf0-43ad-a1ba-69e114b53835
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15260cd9-5450-4073-914a-d426f121a08a
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef2dadeb-fdb3-4f28-8dc0-ad76e60197ea
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff0 && z$w_buff0 <= 1) && (z$w_buff0
      == 0 || z$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01576697-a4a5-453f-8fcc-89365f0cbdbd
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff0 && z$w_buff0 <= 1) && (z$w_buff0
      == 0 || z$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49506583-9789-4df8-bb5c-9b057ddaca50
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff0 && z$w_buff0 <= 1) && (z$w_buff0
      == 0 || z$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e75d7594-6736-4e0e-b56d-8c65836a68e1
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2402751-4947-4a24-b382-afc9b8076874
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fd760d0-59a5-4ce5-a929-491d6cdbb770
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e4bc5cc-4d87-4838-aac2-1af9e9b96a26
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff1 && z$w_buff1 <= 1) && (z$w_buff1
      == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27364a9e-24d9-4c46-b242-e91aa9727813
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff1 && z$w_buff1 <= 1) && (z$w_buff1
      == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e00ba884-e10b-47e7-8b79-071c7ea2ff30
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff1 && z$w_buff1 <= 1) && (z$w_buff1
      == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d9b1cea-3866-4151-9f22-a0f7814199b8
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8007258b-9577-48cc-9c93-1b4873d17143
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4aa2a423-d514-4afe-8a19-5364104ba956
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8c734fb-ef6a-4e04-881a-11582127a9a7
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    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: b9761ac4-cdd3-4883-9881-7458bfc3e3f9
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    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: 7171b96b-73de-4398-8c4e-9864fd71875f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    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: c57158b1-e463-4627-b5bb-152adba75bf6
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c38f604e-61ca-4d7c-91bf-c0ebfff6e8e3
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b38e671a-f02b-4c50-b497-2fec030dd636
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d38c5958-ec0d-4e5a-8132-5412c383d334
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    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: 9bb37348-5826-44a6-a347-dba2ff163ff0
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    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: 3695605b-aa1f-45c9-8395-7e8cd0d901b6
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    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: 1767e064-07d0-4073-8278-7f7b2ee7931e
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae98dde9-6475-4d49-a87b-1df5cf0ba256
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8abd4af-7ed2-481a-b40a-3da3b85699ab
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7dad1a9b-5a2d-40e7-866d-82a3f1170dbd
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43a62415-2752-43e6-a0a6-be1f454d235f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18624dd8-79c4-4398-ba65-35fe7026e0c6
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db45d257-c8aa-4cd8-b2c6-906e78767712
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    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: 39adb1ba-8809-4f33-b1fc-a43a7f2ab506
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    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: 7ae35ff7-97e2-4709-bab1-2624cdc080ed
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    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: 255f4cbf-0541-4d52-94a2-08946d99d9e1
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d52289c-5044-45dd-96bc-d06b779822fb
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23c6b28c-691d-4c4a-b6f2-4305941c898f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 875ff0d2-aa47-45b4-b443-c8cb969c1bcf
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bbe5bec-2b84-44ba-b392-46d9b4fbd22a
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1eb426fd-3d8d-45db-ae05-65baa23e408a
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d393e641-869e-46b5-9dac-ff62e755c9cc
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6435afe-cbec-4321-9fb6-79dc2df7643e
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2409174-8e5d-484d-9e30-aec66aba81a6
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd3c222c-e8f9-43fd-a6a6-ecdfc2f2749d
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7bb2dc0f-563e-4800-8edd-aaf05f076ca2
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e8a4fbf-b967-4f55-b9e0-956173fe7c84
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65dcb061-e42a-4c17-9d43-6f27249895e2
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7921e90-ad77-4e4f-9abe-30324a966fbd
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e99d9baa-ebd8-4022-9dd2-2521c74ae039
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a464ffa3-68a6-44cf-b77a-40c15be8a0ed
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8351cf6a-f069-4ddb-a65b-a3b57fe934ea
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c36a450-10ee-4f7a-bd66-67d0c7eb2140
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 73c8a554-a89d-4c8f-8b9a-a4e770669d62
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8423a657-217c-46d2-8ddd-251a29ebd0f0
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 828
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 40ec13b7-ba3d-47aa-b345-51cbda473efe
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 795
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: adc640b3-1acf-4569-bd53-5da98aff6eaa
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 763
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9900df26-0f7f-4383-b3f3-a100a5700863
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 762
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 17b6c2a4-dc7d-427f-ad16-e14dc53aefc4
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 782
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a3ccda07-6fde-463d-a1b5-7365c4c32fed
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 805
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a28589a-8674-40a9-bba1-446f88ba8209
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 853
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5dfa5345-c1f9-4b5c-89ad-7ddde58277c9
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 821
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 80e2949c-42f8-4f94-add5-ac069aaeb2f2
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 800
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0c2bae4e-8b88-4792-b687-4a0e90f21b0b
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 777
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 15219e77-8287-4dd1-a332-98d4456942f5
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 822
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f51093c8-d699-4063-b396-3b176566a56f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 862
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8411235-3b25-4be1-9e33-0a486368c27c
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 785
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2d2c0e32-70b7-44d8-b15d-18172f36ba88
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 802
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1dd70224-eeb8-48c0-bfbe-405f8fefa057
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 829
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f1c13edb-6dc6-4eca-9561-7dcfa1c6ff03
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 864
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 83cd76d7-2605-4791-bb74-44bbfd6c8e18
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 792
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bbadd073-4b99-4d20-ae6d-23302fa2c591
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 855
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f38047e2-425f-4551-a147-f80a6e5826d9
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 772
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 62d98d3a-a6b9-410c-a7f7-a8f612807290
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 851
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e8a8302f-5443-4837-9c47-7a0f7c80b5aa
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 806
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 992988df-08ec-4c82-99f6-177266938b6f
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 786
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9641d91d-884b-4b6e-a115-38592cb31421
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 769
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 2d3e24fa-3ab3-4913-baf5-c4c59ca05690
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      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: 6726a1db-7e27-4ea6-ac2e-c073a6c3d207
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      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/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 846
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5893139a-3724-4284-abee-a837d9065d0e
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 861
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bbea1f70-c97a-46b9-baf5-49e813a63cb9
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 793
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fae3bb9a-2dbc-4899-8bb6-9bdcaa03a409
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 783
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 18fc9f75-ea84-472c-b8ba-04d1d1d261d4
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 831
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f7b1a1b1-25d3-4a7e-a1be-3f9092ea34a4
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 770
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1f738180-7a61-4afb-b57b-cf455c684500
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 760
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 515edf03-49c3-4fa7-9e38-9faf4f65a845
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 779
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bc804f52-4409-49d9-a1a7-00ba2f85f8d9
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 62aa1591-a781-4ead-b107-1ff830769771
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 759
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 29138868-2f7b-4667-b6ab-1e15b36c6506
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 803
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 54136e8d-c986-4663-9c05-3166d0f19ca8
    creation_time: 2024-04-30T11:17:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix003.oepc.i
    file_hash: 929f303f9fec34ceeaa6ac57212036dd2a2b082a21c34f6b9e4e20069df7c744
    line: 780
    column: 3
    function: P1
