- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e2b72e5-1a2b-40ab-9ea4-00636b43d43f
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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 <= a) && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0)
      && 0 <= z$w_buff1) && __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) && a <= 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) &&
      z$flush_delayed == (_Bool)0) && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd1
      == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) &&
      z$r_buff1_thd1 == (_Bool)0) && z$r_buff1_thd2 == (_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)) && (a == 0
      || a == 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: 4938f74e-910e-4d5d-894e-b3c7444521fb
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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 <= a) && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0)
      && 0 <= z$w_buff1) && __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) && a <= 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) &&
      z$flush_delayed == (_Bool)0) && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd1
      == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) &&
      z$r_buff1_thd1 == (_Bool)0) && z$r_buff1_thd2 == (_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)) && (a == 0
      || a == 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: 6686ad69-a099-4e52-a9dc-37e6be27afdb
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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 <= a) && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0)
      && 0 <= z$w_buff1) && __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) && a <= 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) &&
      z$flush_delayed == (_Bool)0) && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd1
      == (_Bool)0) && z$r_buff0_thd2 == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) &&
      z$r_buff1_thd1 == (_Bool)0) && z$r_buff1_thd2 == (_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)) && (a == 0
      || a == 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: b1648f33-9423-46d1-9d2e-fa369127c147
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 1724a671-34d6-4f4c-bb9a-626d48c8391d
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 452fd49b-2a74-4eac-83bf-61f28f78ebfc
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 49fb9a3b-5008-4724-a3e0-c4a49b4799c8
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 1e62dc07-7499-42fc-9b6a-f3d9b7c75f39
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 43e620f8-299b-4878-8b5d-1101fd505bab
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 93dfc8b7-ba9f-4186-8abe-d5fd4003e236
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34004580-daaf-42c2-94b3-1a4a0142a19e
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b748e632-4aff-423f-8ccf-74232ba5bacf
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34351491-8ca9-4894-809e-bbf9240adc96
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 154fb59c-0276-434d-ab50-d1f7291b8193
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 199e236b-7a44-42d7-b658-9598ee38c144
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 70cf2801-149f-4208-ad55-02f3069e325e
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 36662dc0-2ab9-412d-869a-11a7439344fe
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: e5990ed7-98ee-4067-962a-c4df6abcbaf3
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: be310c3a-a9ad-4782-84f7-9c695683575e
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 297d3709-7950-4a19-ae60-87534d2239d5
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 13738cc8-58c3-4aee-9d38-1abb99987e25
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: fe441af1-a9d8-49c9-96c7-b94c5644a3a5
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: dda65d61-b02c-4ef9-8ef9-2d62c5b65013
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 6a33736a-26b8-466b-b137-aa644fcea101
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: d742624b-3482-4f92-93f9-7e7e21b8fee9
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 6cfcc18b-f77b-4ad5-a0d1-e59c4ec01c92
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: a4a4c613-872b-4ee6-b7ad-c5e43fb8eff7
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: a18bbfbe-6fd3-461f-bf44-ea6f0b4da754
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 9d3f20ac-3f4c-47cd-b4da-f0ce64ea20b9
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 0045cf93-dc20-4cea-ab1d-55d08d2db6ad
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: c67e0af3-bbb2-4459-ae94-09e046a1bbf6
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 045dd339-5585-4f6b-8730-96846b7efd73
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 08d71191-4e9f-49d5-844e-e52e040a98e5
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: cd9e6d0f-3cec-48bc-b569-019a09a1b31e
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 1f881616-66d8-421f-a877-f6382abf7766
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: fafbc554-7951-452e-9fd6-9f5d3f0dcf77
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 34aa2e64-7686-43b8-a58d-98e7e2c9fad8
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 769b1c08-e4fe-4b36-a703-4b5b704e7863
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: b1ff11b5-46e5-4891-b992-89385a32d158
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 2325ea84-deb9-43e6-bd16-dd9bceebd7c2
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: b563dfb4-6437-4915-be84-2df40424dbd7
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 49e5c7eb-b778-4aa2-b30d-5b151d410736
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: e1d44762-ffb3-4fcc-9ba6-1c39f916d656
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 0bb0aa03-eabb-4cdf-a032-e4640755ee55
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 4b02fcbc-3bfe-485b-8db0-e6149c2aea78
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: dae0c342-8bc2-458f-9c55-b018419c0935
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: c7beca0b-dd30-4ed5-983a-d773c33abd7c
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 17825ab6-5b4e-4095-8045-1190f0240cf6
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 6ed17fe6-b846-4787-a602-ff0f176bb15c
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 8f562ec4-f68f-4690-967c-45168d163960
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: 107b02e8-e0b5-40b4-9652-dbeb7ed2d45e
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 9bdc2182-45fb-4f4c-930f-f07d5ad4f318
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 501a71ad-7643-4ec6-81ea-8bd7571886f9
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: b951e094-810e-4077-8b02-6bb63e285a47
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: 19a6847b-bb3b-49b5-b8eb-2af70954fc6c
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 065fa13f-922c-4221-b4a7-769218701006
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa40c658-06c5-4f69-8d36-66c59377f7b3
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a1dfaa7-b952-485b-8880-d2bdd22a3ad7
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: 129b22fe-75bf-4842-9ebc-5459dbb0df4d
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: eeca1da6-0a27-4428-b784-0d8119d65f9b
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    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: e59d6ff0-9c14-4e16-bf38-81be7841176a
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11e885f6-3f57-4efe-b9e4-071a26496b77
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ee27a8f-86c1-489d-b315-b5de903abfac
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bceec3c-943d-4c6d-b9a4-de2fd8ea4dcc
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 856
    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: e1284dae-1c31-4370-a478-2af0fa7cb322
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 858
    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: f1f3765d-8659-434f-8cf6-51188e617686
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6ffa6e13-309c-4b2b-b244-8ba950f1be7e
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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: 05ab1c68-ee4a-4c65-ab76-bdcf787f09da
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 854
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ff949959-9ccd-42ee-a106-944ee8df1168
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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: c247622d-44ac-4289-9a50-92ca7f8f0626
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 810
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 94c061e0-908b-4666-a2be-daf46e932ff8
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 794
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 59611588-31de-42ec-b003-003607f87025
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 826
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f790f479-6493-428f-96bc-d6804b0f81a2
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 869
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a790b99a-f0fd-4d12-99d5-160f0fcca9ed
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 830
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f05c2ab1-fde2-4486-a438-7237ecdf3f6f
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 768
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fc4b8f93-c468-436d-bc05-d2764ed7a8e1
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 774
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f3863925-cb7f-4a81-a205-a2563feb10d7
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 792
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a0ec4a2a-8601-4085-a13e-8f9417f1cca0
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 773
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1b1fb099-69cf-4454-93ee-2e513472c466
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 765
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4fca2cfd-e363-4cf9-837b-035193c59883
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 767
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 74200418-d9a8-46d7-a1ff-6a0fffcab91c
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 790
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 29c6a0e4-c98f-4b99-ba45-ea268788855b
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 758
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5ed5ca21-9fdf-4ee3-9e44-8e14347f9146
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 799
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6627af19-f2b8-4407-8582-ddfbc4e32b62
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 872
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4719e6d8-1982-44dc-9449-86ce30d18e0d
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 760
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 33f6cae3-21f1-4d71-b8ac-04219298365b
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 870
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c2daaa0d-ecab-453f-82c9-3f7d79e9cf6b
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 791
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0f4ca8d8-5679-4905-8373-05330968f4f2
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 752
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 10b3356b-b053-470b-b1ad-a65ed11a0f80
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 839
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 757d600c-3192-4e2b-a69f-d7b9d438cbd7
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 863
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d68cbaa2-1d77-4460-ad10-10685f4e044c
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 755
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fb999d73-fcad-4d5e-856a-476537270a13
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 789
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e814322c-83ed-4acc-bdcc-635bd98ba73b
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 827
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a82a9ff0-5191-4f36-8f34-d4fbfd257e92
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 811
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 74cbf9e9-f202-44d6-97c7-035de91ef323
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 859
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ec6f2a36-57dd-4cc0-8fd2-008599060421
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 837
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c6a89781-2f6b-4c59-86c3-6ce9dcc9ce46
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 770
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8283f731-3aef-4516-be15-a8d30c432cd4
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 756
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 864035da-4b40-4181-980c-8e6b2b7c2a59
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 836
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8a34d57-42cb-4d72-bce1-dd1a06639c05
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 829
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6ae65273-0f60-441a-8c48-bce20b86a129
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 753
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fafa90e8-817b-4e4d-9f38-6641218d43d0
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 757
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9dd31b52-9fff-4b52-9946-46c6ca77f45b
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 27462c23-fa1e-4b3f-8368-2c662f156c3e
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 771
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2554985d-15d9-429d-b8f7-95a322b268c8
    creation_time: 2024-04-29T11:47:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix010.opt.i: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
      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/mix010.opt.i
    file_hash: 371e0ad4620d67bc913500e97f289ec14c56f7c02bd7df3fa28779e14d33459a
    line: 861
    column: 3
    function: main
