- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a9916ca-5d20-4682-ad21-8177678405df
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    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: f048672d-8249-4b54-9f5c-ebd32b3c3ba9
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: 108a1edc-16d4-4b42-8ec7-66ab242a5281
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: b21b9e28-a795-4e9b-9e0e-e3efa10675fa
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: cd7e0041-1823-40b2-a3bd-c08c87e69b3d
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    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_p3_EAX)
      && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0)
      && 0 <= a$w_buff1) && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0)
      && __unbuffered_p0_EAX <= 0) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX <= 1) && __unbuffered_p3_EAX
      <= 0) && __unbuffered_p3_EAX <= 1) && __unbuffered_p3_EBX <= 0) && __unbuffered_p3_EBX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 1) && y <= 0) && y <= 1) && z <=
      0) && z <= 1) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_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_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX
      == 0 || __unbuffered_p3_EBX == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0
      || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0 == 1)) && (a$w_buff1 ==
      0 || a$w_buff1 == 1)) && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (z ==
      0 || z == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4c3544b-f81b-44a9-bec6-519dd349db1f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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_p3_EAX)
      && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0)
      && 0 <= a$w_buff1) && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0)
      && __unbuffered_p0_EAX <= 0) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX <= 1) && __unbuffered_p3_EAX
      <= 0) && __unbuffered_p3_EAX <= 1) && __unbuffered_p3_EBX <= 0) && __unbuffered_p3_EBX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 1) && y <= 0) && y <= 1) && z <=
      0) && z <= 1) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_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_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX
      == 0 || __unbuffered_p3_EBX == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0
      || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0 == 1)) && (a$w_buff1 ==
      0 || a$w_buff1 == 1)) && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (z ==
      0 || z == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd63c3e6-6bc6-40cd-a9d1-22be124a1f01
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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_p3_EAX)
      && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0)
      && 0 <= a$w_buff1) && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0)
      && __unbuffered_p0_EAX <= 0) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX <= 1) && __unbuffered_p3_EAX
      <= 0) && __unbuffered_p3_EAX <= 1) && __unbuffered_p3_EBX <= 0) && __unbuffered_p3_EBX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 1) && y <= 0) && y <= 1) && z <=
      0) && z <= 1) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_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_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX
      == 0 || __unbuffered_p3_EBX == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0
      || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0 == 1)) && (a$w_buff1 ==
      0 || a$w_buff1 == 1)) && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (z ==
      0 || z == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2641ba90-b0eb-4198-aa74-6b452021411f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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_p3_EAX)
      && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0)
      && 0 <= a$w_buff1) && 0 <= x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0)
      && __unbuffered_p0_EAX <= 0) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX <= 1) && __unbuffered_p3_EAX
      <= 0) && __unbuffered_p3_EAX <= 1) && __unbuffered_p3_EBX <= 0) && __unbuffered_p3_EBX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 1) && y <= 0) && y <= 1) && z <=
      0) && z <= 1) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_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_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (__unbuffered_p3_EBX
      == 0 || __unbuffered_p3_EBX == 1)) && (a == 0 || a == 1)) && (a$mem_tmp == 0
      || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0 == 1)) && (a$w_buff1 ==
      0 || a$w_buff1 == 1)) && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (z ==
      0 || z == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab56d711-e453-4698-90b9-494c1f4799ca
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    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: fe3e4d8b-6bde-44d4-9604-cb281129d4ed
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: a8b69829-9111-4758-8aaa-ecc4a7fcebbe
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: bdd68db5-2175-49df-9119-9d142ed6bcb2
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: c568a705-e60c-4b41-90c8-b1a0fd5eeebb
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d8b33ff-578e-4ed5-a077-5256999592a1
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 003be1da-fd6c-41a5-85f2-36895b50c119
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6149104f-5770-472e-9829-9f578cb1bf4e
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9b11601-afb4-43df-8557-63f27d368dc7
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd22eebb-4254-498e-82f3-978d2ce7172f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3f3a85d-1993-4a92-955a-7882e8d2fc1c
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9012eb2f-6f87-4b8f-9e11-d82e9799e663
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fe00a91-a6bf-4ab9-b802-38dc03604d49
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70d0278b-da21-44ac-b201-5d08d19b444b
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78252e82-d38b-4dd8-85c8-51ee8539af30
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5630e4cd-08fb-4604-8a0b-0643f1f67fe8
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4eba1edb-4b37-4522-8a91-e5eef30d138a
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0658835a-1058-4cd6-a061-be1e6d2802b1
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55adb5eb-377b-46b3-a3cf-5e068fe99052
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18fb2888-7fdc-4e68-a932-85ab7f93a498
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec6dca1f-6882-4811-a0c7-236df538eeb4
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f24ce9e-4977-4565-ac63-7392f3d8310e
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: 14fbe570-29a6-4f5b-b45d-0f4d287fe357
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: 9b6a9b9a-fe42-46ff-a412-90b3651e79b6
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: 6f8150ee-87d7-48a0-a839-d8b6a0fa4ada
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    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: 07782ea4-ceb4-4e62-b448-2e58b8be4bb0
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: efc8bcb2-76c5-4420-a273-8866b81ad8dd
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: 4a6f4360-7005-4ac5-b0da-5c605781957d
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: 4c661c60-0b3e-4136-a08b-6466ca3766d9
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a05698b-a216-473c-a9ce-a10fa27950b8
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79b1630e-012d-416a-92ba-5c4db96b6e39
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4448901a-e0b0-41a5-ae95-d8d83d67536d
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8d4867b-1234-4925-b1da-38a366619ec6
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    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: e6d819b9-98e9-4ea1-aecd-140b03dc4baf
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: 18e804e5-645f-444d-851e-ced7f082db80
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: dc5af834-8d40-4f3f-8fdc-eee66e9c6c7c
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: 6b304d1c-8018-4886-9549-5bb4721bab69
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 640290f4-be55-424b-b453-39054ef3a01b
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0dc2665-458c-4958-89ed-909031ba3ae4
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e92cd056-e457-47df-af23-4e0a984c6bdc
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cb49db0-8a1b-4d0d-be33-0153c04726a9
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5832d6fa-5b25-4197-9147-9d96955a5da8
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: b6c4cf7d-10fe-48ce-8615-f15387c20fe0
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: 9a3eabdb-14c4-4f31-9399-8eebb99a9614
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: 8df4b45e-7510-4f1b-b713-a160f06cefe0
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dcccfd8-912f-42a5-bd02-26b414d1ca18
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e377ca7-41de-4de8-ad66-0a04a29dc03c
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96d9ee68-b2ee-4886-b6a5-803fbab851ff
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4aaff9b-8325-42ce-bd63-37e663e4f9a2
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfbc25fb-8337-4937-8902-55c4ca482a9e
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 954177da-d80c-4a26-9e99-5e27abedc1cc
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52958cfb-56eb-4eea-80c4-3004c36ddbbd
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 224b9518-93a1-4546-8f89-7b7cfc645a4a
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7901570f-eaec-4235-9fc8-dfd92c434a9a
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de3d2a98-bfc3-4cd3-951c-b4c41dd28178
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95971208-3236-48fb-b096-d89ff2c1bcab
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 676a356e-d3a6-4b95-97db-32d3ad2fefc3
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    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: e5036d0b-d76a-4cf9-8bbd-f5fe66ced1ff
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: 65976186-fd83-4eb5-ac38-22814334bffb
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: 24f50c13-857c-4cdf-804d-241c2cc4d8cf
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: f556ddc5-c161-4ecb-86c1-189ce7fcedbb
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12ba026c-701f-4a31-b6cb-942042c672bf
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0141c45b-c120-4758-8b98-d7a39ea0936b
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f0f42e7-960e-4f4c-bb60-e65eba5a44b1
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35014c73-814e-43c0-bec5-63776565c4dd
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93390eaa-b4d0-41ec-92a1-30be6bf6aaa4
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6567b3f9-8813-44a8-bf58-3a5eb4da5593
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50266d7d-8da9-430a-a14c-520b79c40b06
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bc31f1e-182f-4657-b37f-1646ffa5699e
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10030498-0cc6-4d8a-9bcf-30d9a31a12b6
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82a6e842-86c8-4652-b3cf-72cdf1275135
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac34c955-fb6f-4b72-b776-e970892db027
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b05e52ce-d7d2-4e23-8a54-a8e29a00cb73
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72d4f898-e78d-4dda-bf25-81bfeaf2a2e4
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: 1315b55b-5a2e-476f-a278-159839718eb0
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: 899fe17a-8452-4c77-acd2-29f03496aa81
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: 97ef4c34-5bb9-4027-b828-f9f73a697796
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d09cb99f-bddc-4b0c-ba54-aac32ac4bb1c
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 034e9b14-ecfb-4ce8-a023-2532cd6cf6a0
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4237ad7f-ec27-4ce6-a066-a42a25272689
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aee76aa1-217b-4ce2-8229-5f421c30b1ef
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13576ada-25aa-4dc5-9f53-c554c451356a
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    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: 69b6cfdf-eabc-4e9d-b8d1-a298b126a262
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    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: 1bf5c9a1-748c-4bc5-8611-8504efaa879e
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    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: 23f15a91-3529-4ad9-9c11-7da10e18dcb1
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ab6288a-91db-4dfd-be64-3d66a015b7d5
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0286a1a-6cbd-4602-a8f4-a4d15ef5ec9d
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47dffc47-b223-4715-a64e-a3a78e2eba5a
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 130756eb-73ac-44f0-b93e-6765fc663cce
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfb03235-e1c5-4899-bb98-b100dff1f08f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0d5fe94-dd82-4187-8a9c-cd1537a4d497
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 880
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87993ec9-d7a3-4f6d-80bb-3a56816d1890
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: cf2c137c-4e14-4fe4-96bf-8254b8f6f7c8
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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: 69540607-cab9-49c8-8f83-c69bffc959f1
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 770
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 75bfe343-e65b-480c-85f3-424fa7c9ce90
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 828
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7cc00a88-05fc-45df-a8cb-483e1a30461f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 780
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 09d0e762-c8b2-45f3-8308-2135802dbccd
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 883
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d770b711-9d66-42c5-9382-291d2ae7273f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 794
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8c3960ef-0e1f-4977-bcc5-7e2d843f22e3
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 768
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c66253b9-4bca-4906-b04e-e40a3733371b
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 891
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cd037838-d891-4e82-92df-26bdbf0cfa36
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 820
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 523c6b96-1897-4b6f-aeab-d60d14304097
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 834
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1e16fb1-93ac-4507-a460-5ec5b207edf4
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 771
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d71fed8f-2163-4b0c-a9fb-a642a354ce8c
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 821
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ca567c9c-75e7-4988-9d7b-94874758df53
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 778
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: edf60a3a-6ac4-4cc4-afb7-48a31bbc54a8
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 894
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6afa3cc9-4fed-452a-aa0b-971538ec4d86
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 830
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7cd3b0df-92d9-45f3-bbb7-848e5ebf43b1
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 850
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3b8aae1e-21a8-4749-9375-420106cc6a16
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 833
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a6f54beb-08d1-4832-9645-6cd2780a7458
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 811
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03ffc571-d224-461e-9b1d-1b583155bd5c
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 857
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2e67107b-eedd-4cf3-8b2a-6c1340cd208b
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 849
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ca2061aa-7e77-4eec-adc2-3ba64e1bb97d
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 823
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fb926ddf-8cc5-4181-a731-f7245a64af9f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 892
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 99ad1770-814f-4ee0-8f4d-b403d8849397
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 813
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6710e28d-5f69-4b2e-be83-376ec4fec7ab
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 793
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1e5b27dc-3249-4470-9cd2-0d53ac859d3f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 801
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 10a2d38f-c5e2-420c-82a7-254fe5765a0b
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 885
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c91b5a63-805e-423d-9256-f651e6b65577
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 856
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9ea6ce59-2407-4a17-9a48-671f1e229c3d
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 791
    column: 3
    function: P1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 26edb552-88e9-4343-b923-112cccd0bfec
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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: b05767c9-bb65-48b2-9b22-1a72450614d5
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 874
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f198a10b-1a23-4144-ae0d-f6547ed822a6
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 859
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7fce05e6-7b2b-4e98-9118-533f9d5212f5
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 800
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3aa56729-57ae-4173-a198-337fce6c9c61
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 790
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5496a3a2-a2aa-47eb-b249-e36bf4f10a46
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 831
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f61350d2-56ef-4a45-b79f-3cd2e423f389
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 785
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 52f33a22-bd3f-4fb6-88d9-2c9339003326
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 788
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eaead0d7-07cc-45a3-957e-c11b2629341b
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 777
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 82f949a9-c6e8-4a2e-9086-fed3a7c469bc
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 881
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 67ce3b96-8f3f-4548-b42b-0ea542622952
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 767
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d15b1191-e1ed-4091-b6c1-5bc378fadf3f
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 755
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ff3b1411-951b-4c0f-a59c-9b0cfb135985
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 810
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ecd07f5a-d9e5-451e-a339-3ab517b5b051
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 803
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f9463574-2412-4edd-bdf0-5d52183e1968
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 808
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d70fe1e2-dfe3-4904-8fc9-20e63fbb86d1
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 814
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 82862514-6e30-4122-8d2e-733cd7261c4a
    creation_time: 2024-04-30T09:57:43Z
    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/mix013.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix013.oepc.i: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
      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/mix013.oepc.i
    file_hash: 39bd8ca48891731a487992488872bfabe93c299f5e64a0d2d763ed7464a4fc31
    line: 787
    column: 3
    function: P1
