- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbb478d3-29d4-4ae4-8de6-9ac22d13fbe2
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: b3fd88e3-fe8b-4316-ba6f-756d6b531027
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 7a3c2e22-2bfc-4c9c-962e-d9a73fb97cfa
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f2f58bd-876a-4719-b8e0-28009093a0d4
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43a23c32-5372-4796-8a26-6952fc15af93
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 65526434-1c52-4ed4-84b0-16b29deeb547
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 8ad53ad1-7680-46cc-9bc5-5cfdc7a15607
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 1c8833b4-2bea-4751-89b0-2c4594722fdb
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: c55cbcb0-36b2-45d0-b9d9-95ce207bbf15
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: f799e093-bb39-4580-9fff-570440756f62
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 0133e7c8-3a13-429e-af8b-999920f1c164
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 8848d03b-7c38-4216-8b03-eda2de29a880
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 7345716c-d4c6-4bdc-b0e5-f53a31b008ef
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: c6434248-b32f-494b-9e5a-c30df0e5b08e
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 350a6273-e426-4bb5-bd16-dbe069298af5
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 1eb87818-ed52-4626-afe2-a2dafb6dc3d3
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5b4632c-4f39-479e-86eb-295629885068
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 4f3a0452-bf50-4cfc-ad41-95f9ca8ef3e5
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: c2089d2a-715b-48c1-9484-f3277a68710c
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: d44ba178-7af4-4814-a28d-c5287b3eb005
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 90284cb6-c59b-4702-9ae4-7ecb56504ecc
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 9f28e2e7-f28b-44a1-8578-ecc50294ae60
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 5d1c9d07-319c-4c3f-b352-264aca5306aa
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: b3ad4ab8-0ecb-4f16-8da5-462773450aba
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: ca29801e-bccc-456e-87cb-1ed374d9dd08
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: a5161c42-30c8-4123-a691-cf01f7eead70
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: b7bd9aa3-159f-41e7-97a7-3ecfdfec8b2a
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 1e818cde-771b-4084-bade-b5f5a1741e6b
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 039b3bb9-dbed-48f1-8a72-313c1db530b0
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: e2b28ef1-1ea6-4b83-9493-be371faf9f7f
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: e1051536-a474-4723-8849-9299465d7f7a
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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_thd2 == (_Bool)0 || x$r_buff1_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a31204a-dcb7-4c51-9c14-47fde71f41c3
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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_thd2 == (_Bool)0 || x$r_buff1_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48991bb4-b026-4046-978e-8bc2aad27240
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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$w_buff0_used == (_Bool)0 || x$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d646ba27-b228-4404-a3ca-41dfa809114c
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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$w_buff0_used == (_Bool)0 || x$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c818b8aa-a906-4fc9-9680-3420e67653d7
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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$w_buff1_used == (_Bool)0 || x$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdd911ee-6e5b-485e-a2ea-c45c08980828
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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$w_buff1_used == (_Bool)0 || x$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e961b23-36dd-4366-9e35-4442408157b7
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 21389615-47bf-4636-9384-f61cf4339b12
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 4e44a40e-1137-4f4d-9a8f-dc363000db15
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 76db5f93-22a8-4f1b-8e25-5a25e7f61659
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 0cfff4c4-375e-4e33-a33d-c503a0e3ae65
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33dd3d2a-7e86-4415-a0b8-edfd3022d582
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6859a3a2-72d3-4482-a04a-245e1d648e03
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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_thd2 == (_Bool)0 || x$r_buff0_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b650b2c5-e8bc-4962-bed5-4a012fc97c34
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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_thd2 == (_Bool)0 || x$r_buff0_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7859f773-f6cc-4523-82db-781d38e6477c
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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$flush_delayed == (_Bool)0 || x$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a42ef823-8566-4355-b5a3-dc480bd16dbe
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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$flush_delayed == (_Bool)0 || x$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0933adee-6d50-4c13-8122-237b455d15c8
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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)) && (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 == (_Bool)1)) && (main$tmp_guard1
      == (_Bool)0 || main$tmp_guard1 == (_Bool)1)) && (x == 0 || x == 1)) && (x$mem_tmp
      == 0 || x$mem_tmp == 1)) && (x$r_buff0_thd2 == (_Bool)0 || x$r_buff0_thd2 ==
      (_Bool)1)) && (x$r_buff1_thd2 == (_Bool)0 || x$r_buff1_thd2 == (_Bool)1)) &&
      (x$w_buff0 == 0 || x$w_buff0 == 1)) && (x$w_buff0_used == (_Bool)0 || x$w_buff0_used
      == (_Bool)1)) && (x$w_buff1 == 0 || x$w_buff1 == 1)) && (x$w_buff1_used == (_Bool)0
      || x$w_buff1_used == (_Bool)1)) && (y == 0 || y == 1)) && (weak$$choice0 ==
      (_Bool)0 || weak$$choice0 == (_Bool)1)) && (weak$$choice2 == (_Bool)0 || weak$$choice2
      == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00fc9155-131b-4d93-b2b3-ca55f86e4be8
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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)) && (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 == (_Bool)1)) && (main$tmp_guard1
      == (_Bool)0 || main$tmp_guard1 == (_Bool)1)) && (x == 0 || x == 1)) && (x$mem_tmp
      == 0 || x$mem_tmp == 1)) && (x$r_buff0_thd2 == (_Bool)0 || x$r_buff0_thd2 ==
      (_Bool)1)) && (x$r_buff1_thd2 == (_Bool)0 || x$r_buff1_thd2 == (_Bool)1)) &&
      (x$w_buff0 == 0 || x$w_buff0 == 1)) && (x$w_buff0_used == (_Bool)0 || x$w_buff0_used
      == (_Bool)1)) && (x$w_buff1 == 0 || x$w_buff1 == 1)) && (x$w_buff1_used == (_Bool)0
      || x$w_buff1_used == (_Bool)1)) && (y == 0 || y == 1)) && (weak$$choice0 ==
      (_Bool)0 || weak$$choice0 == (_Bool)1)) && (weak$$choice2 == (_Bool)0 || weak$$choice2
      == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12bb296e-a062-40e1-88f6-c9913e58df2f
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc473db7-61e9-4105-b478-9989054bcb44
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e80fb814-7c9f-4a8f-941b-274dc26f1d91
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c7b5b6f-6656-4445-a7c2-2b7043c0f870
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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 || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9c9b5d29-b133-4ef3-ad25-3ef8524549c8
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 81210ab8-6e65-4ae7-9d5d-3fddd02ed6fb
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 5c89984d-3e0a-47d9-843c-6206b07fde81
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 2ac42e44-e9ab-4482-8588-79c20789770b
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 53831af7-c16c-4f9d-b365-2f799c97ae00
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 0183685d-0538-42d2-bb59-3136ffd11541
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 4e1ced50-7562-4d29-910f-ea62dbbe0dd0
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 43746931-2701-41f3-8e37-1a888bc27b0f
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 5ade9d0c-1887-44d0-b224-b4c78029de7f
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: f504192f-cb65-430b-9eda-60592d97ba16
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: bf5dfaf0-0ebe-4316-8043-8176b31264f6
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 81fab64e-b8f5-4181-be6f-d19587f08e18
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 479b94b1-e057-45f3-bdd7-1da00f8e5b47
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 2ac065c6-df49-4f72-b0e6-74320f81e0b0
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 79123106-e16f-46c1-9c1a-c7b8cea4d3f5
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 8b82e14f-8a32-4910-be22-c631816dc945
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 204b4873-4f06-4591-98bb-ca23bdfd581c
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 78ab730e-8df2-4d28-9a1a-09a33b452d75
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: b1f23828-8dc3-41b5-8bd6-12c05857fdfd
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: c1df7329-fd76-483c-91b1-eae2eef6c939
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: fc978ca7-f57f-447b-9903-5b3b1875a213
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: a29295fb-59ed-4be2-bfe1-b6a2f94c78ad
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 4e0fcdad-7958-4fad-a9ba-8dad8bb53bb2
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: d636fb14-257f-46cc-be0f-89273fa05e8d
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 96c281c6-906f-471f-a099-bf2f4638ca63
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 1bb0fd2a-945d-49fb-aaf9-b17c87252317
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: d517cd71-c3de-4fec-81cc-3891f8369470
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 60677302-de9c-4cfb-b6b0-0f8c59ff6bf0
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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: 277f9269-05f5-4f96-b1d4-b88537098470
    creation_time: 2024-04-26T10:39:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/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
