- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a8bf5f8-0c4c-4fcf-92d0-d5fbdf613b39
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p0_EBX)
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX) && 0 <= x) && 0 <=
      x$mem_tmp) && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && __unbuffered_p0_EAX
      <= 1) && __unbuffered_p0_EBX <= 1) && __unbuffered_p1_EAX <= 0) && __unbuffered_p1_EAX
      <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX <= 1) && x <= 1) &&
      x$mem_tmp <= 1) && x$w_buff0 <= 1) && x$w_buff1 <= 1) && y <= 1) && x$flush_delayed
      == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0) && x$r_buff0_thd1 == (_Bool)0) &&
      x$r_buff1_thd0 == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$read_delayed
      == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1)) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (x == 0 || x == 1)) && (x$mem_tmp == 0 || x$mem_tmp == 1)) && (x$w_buff0
      == 0 || x$w_buff0 == 1)) && (x$w_buff1 == 0 || x$w_buff1 == 1)) && (y == 0 ||
      y == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1ac0469-cca6-4351-994f-5ea34e6c3a6e
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p0_EBX)
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX) && 0 <= x) && 0 <=
      x$mem_tmp) && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && __unbuffered_p0_EAX
      <= 1) && __unbuffered_p0_EBX <= 1) && __unbuffered_p1_EAX <= 0) && __unbuffered_p1_EAX
      <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX <= 1) && x <= 1) &&
      x$mem_tmp <= 1) && x$w_buff0 <= 1) && x$w_buff1 <= 1) && y <= 1) && x$flush_delayed
      == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0) && x$r_buff0_thd1 == (_Bool)0) &&
      x$r_buff1_thd0 == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$read_delayed
      == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1)) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (x == 0 || x == 1)) && (x$mem_tmp == 0 || x$mem_tmp == 1)) && (x$w_buff0
      == 0 || x$w_buff0 == 1)) && (x$w_buff1 == 0 || x$w_buff1 == 1)) && (y == 0 ||
      y == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d4ede64-79cc-4f37-a47f-02f416e42f40
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c723be1-29ed-4f26-9d67-6922f9db5ca2
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64f36f45-5bc7-416b-b116-94ddc83b96d5
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9528179-eeb4-4e62-b65c-bb8fc54c2be0
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e22f0ba-1b7f-4080-9bab-6104fa3184ef
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2befc39-3351-4254-b327-fda60b029f41
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 220d0d54-d99b-4180-ab27-ecdab2608a28
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db45c53e-215a-47c8-b6ca-5410ba3cdff2
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb704ab8-30d2-4b03-8cec-aaa5eaa51256
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    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: e0603ae8-5fcd-423f-91bf-8a583c1db1fe
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    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: fe8c13fe-ee96-4017-a96b-dd2afacd3368
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    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: 0c3e5055-38c9-425e-96b2-53523ee1da4b
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    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: e7b35b18-37fa-4b7c-8f40-05aa20c83655
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f31bdf28-a18c-4db1-a837-eea29390938f
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d745ec21-5fff-4d31-b28d-8d9ab1f7ceca
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EBX && __unbuffered_p0_EBX
      <= 1) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a784792-7cb9-4c75-8e0b-2f4eb9bcf62b
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EBX && __unbuffered_p0_EBX
      <= 1) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acbd681e-c064-4b4b-b416-94b776dfbd3b
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57754958-17ec-41ea-8e5f-b53165b4d966
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a891b30c-d5b5-49eb-b201-4f89fa417313
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eac52f98-4cb1-402d-8a8d-37512294ade9
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89f0bbc8-a5b9-4258-af1e-8a81c9aa3db0
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c857c898-67de-4f95-a6e7-96b105fd8121
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 026adff0-f531-4a73-9172-b8a1547592c2
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff1 && x$w_buff1 <= 1) && (x$w_buff1
      == 0 || x$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3ef495c-ac43-49d3-8057-f19e807d70ba
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff1 && x$w_buff1 <= 1) && (x$w_buff1
      == 0 || x$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2822fde-3240-4cb1-820c-a48b95df098a
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    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: 43591f19-252f-40c0-a3d9-3eb13e2f1aed
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    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: 32622f15-6d75-4f3a-90b1-e8b5d74676f5
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 1) && (x$mem_tmp
      == 0 || x$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f46dcccb-172d-43e9-b47d-72425e766f41
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 1) && (x$mem_tmp
      == 0 || x$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2964242-81cb-48dd-a855-e798d76c6cbb
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 515481b3-c4ff-424e-bbae-925f52330594
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6380c942-cfe0-4906-b6c0-77f92e38417f
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff0 && x$w_buff0 <= 1) && (x$w_buff0
      == 0 || x$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 897a7f0c-ffd8-4b68-bf43-b940a3e9ddee
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff0 && x$w_buff0 <= 1) && (x$w_buff0
      == 0 || x$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: dd4411b9-c90d-479b-b654-0ce6b6e54af9
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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: 775f19f1-63fe-4346-a48a-e5a7d2e7d020
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 834
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3a3ef519-87c1-4363-85d1-a3de437270dc
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 763
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6ae1f69b-e7f4-423e-8cb0-c1261b00b398
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 840
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 139082d5-e0e4-49ba-9cb9-e5cb6152248e
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 784
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a12d080-0dd6-4536-8a47-394500dc34c3
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 803
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e460920c-ab04-4e1b-893c-011e67a77014
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 841
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 54290648-d308-46de-83b9-a11c904ae9f3
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 764
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0958e5e4-b7c8-4185-b2b6-f5da45e04d1c
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 812
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5a4a996d-bdd0-4fc5-89f2-8409ef83715f
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 843
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cd488c33-1f3b-4ba8-b1c4-214be5919ffa
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 744
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c35e5d6a-448e-40d9-9fa0-7af102ff7133
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 802
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 44dd69fb-0af7-4567-91a4-f42a0deddbc2
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 766
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: db74b8f7-4413-4566-a0e6-13fbf9ac27ed
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 809
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 119df546-9dc8-4220-b6e1-f8eba42c04e8
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 768
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 11bdb449-b68b-4376-bb85-3a16ed6aacb5
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 747
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e242f8a1-4e31-4d4f-8f88-d3ffadc85cf2
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 800
    column: 3
    function: P1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ea4bd60b-97d3-411e-ba5f-6c5b936d9bbc
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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: 116101b5-ec2a-44ea-ae17-35d7e40a71bd
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 827
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cdeb08db-3480-4d2e-a349-4f0c90c8af29
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 783
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0573327-01ea-4a0d-a7df-9f711174c991
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 765
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4d3a6ec0-9bc1-421e-b52f-e5a081250f48
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 773
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 303812b6-93c2-4f3c-b271-6d6bc1a42395
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42b1a4b3-ee06-442a-9560-5660720d02ce
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 832
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9f402ff1-c218-4bd7-8b7a-76c47e8c3aae
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 745
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e12f65d9-88fc-4e05-a022-90a1a707af26
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 799
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 31b87379-9a43-48f5-8c66-d34264efb3ed
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 742
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e23b8b37-bc50-4802-bbd1-fd1347961a84
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 830
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 85628c0c-a951-46d2-ab61-ba535e2651d0
    creation_time: 2024-04-29T11:46:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix000.opt.i: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
      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/mix000.opt.i
    file_hash: fd6a5bc5d3f013f4ace97b77d830608c8280eaa5bc8f461c3acae231027617e4
    line: 810
    column: 3
    function: P1
