- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35d8f628-a7c0-40be-b8e2-a08e3f1d4899
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX)
      && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX) && 0 <= x) && 0 <=
      y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0) && 0 <= y$w_buff1) && 0 <= z) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 2) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX <= 1) && __unbuffered_p2_EBX
      <= 0) && __unbuffered_p2_EBX <= 1) && x <= 2) && y <= 0) && y <= 1) && y$mem_tmp
      <= 0) && y$mem_tmp <= 1) && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1
      <= 0) && y$w_buff1 <= 1) && z <= 1) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0
      == (_Bool)0) && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) &&
      y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd2
      == (_Bool)0) && y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (__unbuffered_p1_EBX
      == 0 || __unbuffered_p1_EBX == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1)) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y == 0
      || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp == 1)) && (y$w_buff0 == 0 || y$w_buff0
      == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && (z == 0 || z == 1)) && ((__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX == 2)) && ((x == 0
      || x == 1) || x == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93a32982-cc1d-4b3e-aa99-0e41d8e035c5
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX)
      && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX) && 0 <= x) && 0 <=
      y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0) && 0 <= y$w_buff1) && 0 <= z) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 2) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX <= 1) && __unbuffered_p2_EBX
      <= 0) && __unbuffered_p2_EBX <= 1) && x <= 2) && y <= 0) && y <= 1) && y$mem_tmp
      <= 0) && y$mem_tmp <= 1) && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1
      <= 0) && y$w_buff1 <= 1) && z <= 1) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0
      == (_Bool)0) && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) &&
      y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd2
      == (_Bool)0) && y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (__unbuffered_p1_EBX
      == 0 || __unbuffered_p1_EBX == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1)) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y == 0
      || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp == 1)) && (y$w_buff0 == 0 || y$w_buff0
      == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && (z == 0 || z == 1)) && ((__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX == 2)) && ((x == 0
      || x == 1) || x == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d260336-65d9-4368-a2dc-e3b78a2f3b20
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX)
      && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX) && 0 <= x) && 0 <=
      y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0) && 0 <= y$w_buff1) && 0 <= z) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 2) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX <= 1) && __unbuffered_p2_EBX
      <= 0) && __unbuffered_p2_EBX <= 1) && x <= 2) && y <= 0) && y <= 1) && y$mem_tmp
      <= 0) && y$mem_tmp <= 1) && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1
      <= 0) && y$w_buff1 <= 1) && z <= 1) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0
      == (_Bool)0) && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd2 == (_Bool)0) &&
      y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd2
      == (_Bool)0) && y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (__unbuffered_p1_EBX
      == 0 || __unbuffered_p1_EBX == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1)) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y == 0
      || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp == 1)) && (y$w_buff0 == 0 || y$w_buff0
      == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && (z == 0 || z == 1)) && ((__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX == 2)) && ((x == 0
      || x == 1) || x == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6169a025-b106-4e63-b2a7-96374c7c01ca
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98a56f5d-5226-4b82-a6f3-27834cc735d6
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0419169-2bbe-4780-b02c-60a2aa313bc6
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe5bfbef-b753-40d8-9dc8-3aded7ccc25b
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    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: 42b3e8e1-b7a0-464c-bce2-b2529b85e3c8
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0496f75-3353-46a8-867b-88643149965a
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    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: fb723e42-4fe0-4442-93a3-514e3507d6cf
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef9d5531-d9eb-433a-a6d0-420fd0685e87
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55ae71e0-e851-490b-800e-5f046c7df143
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf69db85-2819-471a-8a51-6235a11b129d
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc815679-18c2-4d5a-b994-84006de291bb
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 543280d2-fa75-44ef-88da-e9d3c70465fb
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2200e953-c564-4ed3-ab42-08d1ef187e0b
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    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: 9211bb59-c913-44c9-9405-4cf87a743696
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59e32f54-66c5-45b6-a6b1-8cd7e52bd9c7
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    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: 4ff72bb9-217c-4dd7-930a-cc62ece7256a
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5e62a5a-b5a9-4224-8494-4acbc5cd9bc7
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 732ec594-8160-4e1d-a79e-c74510f1a697
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56990e42-d9d4-477c-a495-a7da12711677
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    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: cdb9f376-fa0c-4c64-84d7-72cf71c9edbe
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0200f6e7-0b49-4a73-a0b7-27f452a8dd82
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    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: ab4927b6-0fee-4fff-97b5-00d877aef0a7
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 759c7b9d-e1a0-4445-bb90-93f05b4f3bc1
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bec744bf-f329-405a-b9c4-68e48de0a81b
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29a9e9b1-6222-4b05-bcdf-2073101c0da9
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e5a7d2b-20b9-451b-92ac-9928bd9e8f39
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bb6e3b9-2172-4ec5-ae16-15f0a30f2fbd
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa6912ee-fed0-42dc-84a3-38d97bce6c3f
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    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: 5bd63308-1edc-45ab-8c7f-689ea08492f3
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 805a950f-a119-4a2d-9489-d11ed7d9e804
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    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: 82d56689-a3f6-4717-af3a-95c850ea71cf
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 2) && ((__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17a98158-66c6-418e-a5d7-e005ff410240
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 2) && ((__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3283c1e4-c5d1-49ad-85d7-72988ec3df4b
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 2) && ((__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5591f39-4bb3-4446-be8f-64cdff87153d
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b074f02-ca5d-404e-8fe2-44990d494fbc
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce9c6724-bdb7-402a-8680-3a9e99ed2c80
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 655fabab-f51f-499b-aa4f-9054f733518a
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a085b7c5-caf3-452a-af7d-db6e7bf037bc
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bca99821-8292-40c2-ae69-0a7153410ece
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2222b2a7-77fb-47e6-91ca-1bca2fe961f3
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af97ea25-a868-4129-b553-2f52b91e8d12
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2915e50-405e-4024-90f7-4cecd0240269
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4829e7bd-c571-4247-8fcd-009d4ed27337
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    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: 8d0d4690-4b89-4f74-8ba2-66c40b9f3ec7
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db1505f7-f44b-4f7a-9e11-f79069928290
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    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: 1ed51c34-ec0f-4ff0-a759-406fd86426ec
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33906de3-54a2-4f4e-a728-a3bbec1c8439
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 027222a1-877e-44de-ba8f-ee7dee802c5b
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acee780f-f4da-49fa-9242-4db348f1d00a
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24e152be-8fd8-4165-adb5-93e5f5a7d6d9
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63e92087-8d00-44e5-b0bf-674d41e0fb5c
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32288153-7d85-4267-a43f-3f40135fefea
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d7e3f8b-d0cb-4c0f-af4c-ef30f9c7bb55
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5626bae-3794-4de1-8354-7f5fdec0f625
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b968ef3b-3a02-4a80-a596-41d84eecdf0f
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad20bd1c-d69e-4e33-80a1-cfef1e266b86
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecae8986-d530-426a-8be7-405b98cc782d
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 30ed051e-7d23-48b0-9aa5-28232c5cc44c
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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: 0e5dfec8-05be-4a4e-9760-ba773a706354
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 852
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 29078e67-f8c7-42ae-87ef-95608ce99928
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 792
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a1aebf36-2c0f-42fb-8614-70c0fa9f4483
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 822
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 93af4eae-9492-45a8-9e5a-3d933e7b6060
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 804
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: da093644-dd2c-4d9a-a399-97ac0ebcc112
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 863
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2969c4ab-2be3-45f3-8cd1-373541cc9247
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 830
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1fc69172-0695-4264-950f-743ef8adbf27
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 764
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aca65135-b8f3-4b4a-bc73-330b7c47a48a
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 820
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 85bb71d5-2696-45e5-9df4-f5e270280cc3
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 829
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 61b0c2b0-44eb-49c2-87f3-1ccbd84193a5
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 761
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 95c909a3-7503-4de3-ba4d-f2bda106048c
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 763
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 009222d2-6c30-40d4-8044-228ef8783564
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 754
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b6cb67e2-65eb-4ce8-88b2-da926d8eb4ca
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 756
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f54d813d-cdfb-4785-a259-257ade907b53
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 783
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3ccff303-075c-46d9-8c78-2c58a129a85c
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 862
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e7b525b0-10ce-49fa-97b4-abcc2f8623fa
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 784
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 68fb6402-3b4c-49e6-bba2-259c7e137cb6
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 787
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2e718dbe-cc5a-4065-998b-09ff7cd69925
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03f6f8a8-9f43-42fc-9bc8-672780b37b37
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 782
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: df9eea04-163a-4b09-a11d-0d8fe977bd66
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 803
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 87bf29d9-3e11-47ff-82bd-debce8f8ba26
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 865
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 25bccae5-b7cc-4569-b6d7-53ed220877d7
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 854
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cd92c745-5345-476c-8b75-318ff7465294
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 751
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ac5ff01a-3a62-488c-9abf-6ff21cf1a710
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 785
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 19a1e38c-1d39-424a-9bd3-c5a8edf45ad0
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 823
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5252fa4d-7fc8-4690-9b80-cc3d7652b92e
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 819
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c40191d1-98cd-4091-ae69-46f96f540276
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 856
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: d4cc1bbc-d4c4-41af-8452-e201254d1887
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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: d01aa21c-24d9-4f08-8e22-cd5a6dd246ba
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 847
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 97d8aac3-a4fb-4831-9ef7-d2b82a2a8c9c
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 766
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bfed54fe-7c1f-45d3-979a-125019dee657
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 752
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 48fd69dc-63ed-4249-b1c4-dbf70fd9116e
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 832
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 18d6de4f-ef51-4a3f-beb5-dbd857d6a9fb
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 749
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 133e7073-c219-4bab-8acf-01e4bf5f57a0
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 753
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 80586abf-c60d-4254-8822-6aeb5b255392
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 746
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ea548a03-64bf-4574-b4c5-6882e2ac18c9
    creation_time: 2024-04-30T11:18:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix006.opt.i: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
      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/mix006.opt.i
    file_hash: 557c1f2fab4f7585e181c0a50145e0f2efcca52cad7f093489c012afed407365
    line: 767
    column: 3
    function: P1
