- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d232c2aa-f851-4b61-98db-96ad2b2bc249
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: 6731bc1f-becf-4a54-94d2-c7c307b31ead
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: e5f33a9e-c0e3-4056-8878-e8f7190948eb
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= x) && 0 <= x$mem_tmp)
      && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && __unbuffered_p1_EAX <= 0)
      && __unbuffered_p1_EAX <= 1) && x <= 2) && x$mem_tmp <= 0) && x$mem_tmp <= 2)
      && x$w_buff0 <= 0) && x$w_buff0 <= 2) && x$w_buff0 <= 127) && x$w_buff1 <= 0)
      && x$w_buff1 <= 2) && x$w_buff1 <= 127) && 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) && x$w_buff0 % 2 == 0) && x$w_buff1 % 2 == 0) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (x$w_buff0 == 0 || x$w_buff0 == 2)) &&
      (x$w_buff1 == 0 || x$w_buff1 == 2)) && (y == 0 || y == 1)) && ((x == 0 || x
      == 1) || x == 2)) && ((x$mem_tmp == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60ad778a-1658-4712-bd72-ee502976f79f
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= x) && 0 <= x$mem_tmp)
      && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && __unbuffered_p1_EAX <= 0)
      && __unbuffered_p1_EAX <= 1) && x <= 2) && x$mem_tmp <= 0) && x$mem_tmp <= 2)
      && x$w_buff0 <= 0) && x$w_buff0 <= 2) && x$w_buff0 <= 127) && x$w_buff1 <= 0)
      && x$w_buff1 <= 2) && x$w_buff1 <= 127) && 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) && x$w_buff0 % 2 == 0) && x$w_buff1 % 2 == 0) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (x$w_buff0 == 0 || x$w_buff0 == 2)) &&
      (x$w_buff1 == 0 || x$w_buff1 == 2)) && (y == 0 || y == 1)) && ((x == 0 || x
      == 1) || x == 2)) && ((x$mem_tmp == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8126608-7acc-48a2-ac7c-97cb77b79fab
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff1 && x$w_buff1 <= 2) && x$w_buff1
      <= 127) && x$w_buff1 % 2 == 0) && (x$w_buff1 == 0 || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95e166c1-df09-4790-8798-3e125b39c4d8
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff1 && x$w_buff1 <= 2) && x$w_buff1
      <= 127) && x$w_buff1 % 2 == 0) && (x$w_buff1 == 0 || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a607def-ce49-4332-87e9-afc1b2815152
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f427d6d0-b00a-4cc6-9daa-6c3417a17832
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31942d08-e0d0-4eed-8dae-830f4c4fe8bc
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: cc060332-1634-4625-8ca2-eec35817800d
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: 27f03a94-45f1-45a7-8d70-001d9019cbe9
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: 71de8c44-dab8-4b2e-8fbb-a03fc469d5a4
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: 3c0ac034-1e4d-424d-88a1-11f5f062d45f
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff0 && x$w_buff0 <= 2) && x$w_buff0
      <= 127) && x$w_buff0 % 2 == 0) && (x$w_buff0 == 0 || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4146608a-e8b9-4222-a429-f3b7c4758702
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff0 && x$w_buff0 <= 2) && x$w_buff0
      <= 127) && x$w_buff0 % 2 == 0) && (x$w_buff0 == 0 || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5dfadba-aa85-4614-bc52-bf36d8f90bec
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: d6cf10d8-80cf-42e6-a292-cbf519a65504
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: 05ef0d01-d044-4e27-8dde-2fb2cb39fb68
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: f4491b67-add6-4f75-b3c3-68ee6d229716
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: c9ccc61a-bbca-4ffc-8fc8-b97ab8b26923
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: faf3ca58-2631-4d75-a097-3d407542b581
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50092f0e-f6e1-4add-834c-74ddaad6b7e5
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: 37dc256c-1502-4079-9ff1-cfe622e5b603
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: d4e26e56-c9c6-4e2a-9d8b-e561a2998170
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: 2073dd21-6868-4eb0-974e-e866b4cbc8cd
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: f55cef4c-b580-4a4a-b4e4-bd9e8d2f0dbb
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: 6803479b-9e50-4362-b978-f09e6f375761
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    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: 90513121-8afe-4505-8d89-add1661a1faf
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 795
    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: cbd4ae3d-ac6a-4f8d-adf3-312bbd09d28b
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b04d5f34-9045-4bc2-828c-2f11f907f9b8
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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: 533df13d-2ea8-421c-9e31-2217079bded7
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 747
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c4c18a3b-8320-4ab1-aa4c-be8d5900570f
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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: 56c40d83-f928-4277-86eb-c43723c75455
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 793
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f091271c-9e75-4461-bd37-50fa95cbc52d
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 740
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f415189c-f271-488d-a712-669fbe5133c2
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 775
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e0608179-4e0c-4d86-8f82-d64952df37d2
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 807
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 35b8bd29-226d-46df-b62a-a56a3058dc4e
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 769
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ca88522a-9938-4e40-a33f-30206c66fdcd
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 800
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 83f880e5-c7b4-46fe-82c9-da7e2e69cdbc
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 765
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d536750c-6e85-461f-9901-9b046ca069f7
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 65f40b0b-e92d-4cdd-8294-497afb251a27
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 768
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ad3b5553-e23e-419d-9622-1ace02b35866
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 741
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a8d1310c-64fd-4605-b755-6f2ee7630885
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 778
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cb2eca44-c9e0-4ddc-a234-cec1b3210c0d
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 755
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4355ffda-0352-43a3-b003-4d3a134b7c69
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 776
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 33a4313c-2fc9-4ccd-8fa3-eb65faaa598f
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 806
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2ca200dd-035e-4484-9620-8c07d34dcaa4
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 822
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 05d0b8bb-db13-4bc8-a6f6-f37055b39a52
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 737
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6bc9f83b-a276-4210-bccc-90ad4f40da6d
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 738
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 86f2fdfb-98d8-48ed-a1a2-cc2aa6a0032e
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fb888620-b339-4a2e-9063-c3c95536969e
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 766
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a5d4f9b-3299-482e-9435-055e647eb322
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 735
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 14ee2a6f-f451-4e69-b4b2-cab844ee2792
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 798
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7446d21b-8af7-4749-a9eb-29aed1d6d239
    creation_time: 2024-04-30T09:59:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
      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/mix054_pso.opt_rmo.opt_tso.oepc_tso.opt.i
    file_hash: 4b807ac1723767f46eb51e856f642cbeec29c757d6219d60986235d902b15355
    line: 796
    column: 3
    function: main
