- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0d3505b-b134-46bf-9346-939a9153945b
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX)
      && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0) && 0 <= y$w_buff1)
      && __unbuffered_p1_EAX <= 0) && __unbuffered_p1_EAX <= 2) && __unbuffered_p1_EAX
      <= 127) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX <= 2) && __unbuffered_p1_EBX
      <= 127) && x <= 2) && y <= 2) && y <= 127) && y$mem_tmp <= 0) && y$mem_tmp <=
      2) && y$mem_tmp <= 127) && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1 <=
      0) && y$w_buff1 <= 1) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1
      == (_Bool)0) && y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (y$w_buff0
      == 0 || y$w_buff0 == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && ((__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX == 2)) && ((__unbuffered_p1_EBX
      == 0 || __unbuffered_p1_EBX == 1) || __unbuffered_p1_EBX == 2)) && ((x == 0
      || x == 1) || x == 2)) && ((y == 0 || y == 1) || y == 2)) && ((y$mem_tmp ==
      0 || y$mem_tmp == 1) || y$mem_tmp == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a86a705d-8ae9-45cd-aca0-3aa2afece010
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX)
      && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0) && 0 <= y$w_buff1)
      && __unbuffered_p1_EAX <= 0) && __unbuffered_p1_EAX <= 2) && __unbuffered_p1_EAX
      <= 127) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX <= 2) && __unbuffered_p1_EBX
      <= 127) && x <= 2) && y <= 2) && y <= 127) && y$mem_tmp <= 0) && y$mem_tmp <=
      2) && y$mem_tmp <= 127) && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1 <=
      0) && y$w_buff1 <= 1) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff1_thd0 == (_Bool)0) && y$r_buff1_thd1
      == (_Bool)0) && y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (y$w_buff0
      == 0 || y$w_buff0 == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && ((__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1) || __unbuffered_p1_EAX == 2)) && ((__unbuffered_p1_EBX
      == 0 || __unbuffered_p1_EBX == 1) || __unbuffered_p1_EBX == 2)) && ((x == 0
      || x == 1) || x == 2)) && ((y == 0 || y == 1) || y == 2)) && ((y$mem_tmp ==
      0 || y$mem_tmp == 1) || y$mem_tmp == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82464930-8878-4b2b-961a-6b8654c62dab
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3d2cbe8-8cbe-4995-b766-18c222bb8550
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15287dd2-077b-4439-bbdb-4422bc35f0fc
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3266b55-c21e-453d-b21d-c7324cfaf368
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b921d1b-277d-4ef1-8919-3ad45b51b707
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 398f0bda-fed1-4324-a934-7b21c7226775
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb658844-d7c2-460e-84ab-2c6a4b5c10b0
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8836d8d-a326-475e-9afe-5ea479afbd3a
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44e02abd-c8cf-4fda-8584-d3841cd26464
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 2) && __unbuffered_p1_EAX <= 127) && ((__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1) || __unbuffered_p1_EAX == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ced0a83b-d89f-400b-b809-b2c7ae1ad0a7
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 2) && __unbuffered_p1_EAX <= 127) && ((__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1) || __unbuffered_p1_EAX == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2d3c06a-1c07-4ef6-9ac7-b7a8c926b56c
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 424e6876-1784-47fa-ba18-3dbd88414272
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y$mem_tmp && y$mem_tmp <= 2) && y$mem_tmp
      <= 127) && ((y$mem_tmp == 0 || y$mem_tmp == 1) || y$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f48faaf-f246-4ad2-bd3d-dbe4cde7019c
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bd89598-8be8-47b1-827e-6b93ba949476
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab61c48b-a249-4de1-82e5-9614d1cd6c85
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73f6a3da-f725-4c30-a9f2-d9df640370b6
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0737b97d-d292-4a9a-b750-82338fda173f
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68d22a89-252b-4682-bbc2-b0686499cc38
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03f660ad-eb20-4f02-a4f1-a57eb78a9908
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 497c23d5-a065-4a70-9d10-bc449b3df31e
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6447b0d6-3964-4ca2-b5ab-fbaf94b1d778
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d59e3e0-12ab-4ed5-86bf-dde2bb0093d1
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b504a274-4e3d-4a64-84eb-cf43d9c37d01
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33874f12-c571-4e55-9463-067490987f00
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d210f096-8149-4c5d-916a-8c99ab3a1b2e
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 829
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 2) && __unbuffered_p1_EBX <= 127) && ((__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1) || __unbuffered_p1_EBX == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 576a05de-1e6d-43b5-8c86-fc8fe189c320
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 2) && __unbuffered_p1_EBX <= 127) && ((__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1) || __unbuffered_p1_EBX == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e15bf30-3fd6-4bfa-b62b-3e6510ff274b
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    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: ddaf3485-2b76-4761-b663-2d0f4fb8f6fa
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    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: f5a3d037-2acd-4513-b511-eecd4f692212
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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: 7ef72edd-7270-4d22-83b6-17ce1a91fa98
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 749
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7e754227-a469-4696-b9ca-685a1bae575a
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 760
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e14f8d46-fe71-4beb-9c16-46b43cf17b50
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 810
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e4220e16-7978-4432-aedd-fcb16152d948
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 802
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f2df14ab-b418-4d08-acd0-a708db678f66
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 786
    column: 3
    function: P1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 340a3a5c-a5b9-4bd7-b68b-97094e6ccbe2
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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: ef85750e-7a5a-4b4f-b10f-60b966afda4e
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 827
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 06cdb098-d463-461f-be0b-7eeae2c63c2c
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 812
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5da06d4f-087f-40b2-afb3-ccf5b7e6efbc
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 771
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fe643af4-eeb7-4ba0-8507-2ecbb0e6e8b6
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 841
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 903d3fbb-68d3-48e1-8f0c-b6dd7e0d7609
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 787
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 24d8ce9e-4527-4a1b-b794-16b90139cb9a
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 752
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 65e6a7f3-5950-4f20-9e0e-1203b09229eb
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 759
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 74afed0b-e587-4de6-9cce-5e8f60b6c44c
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 739
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a070c0bb-e07a-49e8-9201-27ab5c9f1ba0
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 742
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3a89b551-a7d5-4915-bf2c-63ef8ebe4ca1
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 856
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42b91161-226c-4c9a-915c-78291052c81a
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 803
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1b418221-a141-4cb2-abf8-86dc24d62874
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 809
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ca5db58b-cf36-453e-9273-8121e13cf03b
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 840
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 446829ac-cd4d-4f09-9f49-b72b8c4f4d0e
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 830
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 01ca08fa-72bc-4c41-8ad9-f05cc179a1fe
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 832
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a6dcbf7b-4ae4-44de-8422-6e06be3aba9f
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 770
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 88bccc7d-57af-4c1a-9576-a078713ba456
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 743
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ef4e83b6-230f-47f7-97b2-0882c1323275
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 834
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4ada6473-eacd-4b12-a406-72b1d65ba155
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 757
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1e5a4e3a-c2b8-4694-a348-5c4d7b92e239
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 740
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b17616cc-7c2c-4b74-b0a9-78c981130e4b
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 13004368-4dd9-4ec9-9654-54d8d1513ca5
    creation_time: 2024-04-30T11:20:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi000_tso.i: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
      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/rfi000_tso.i
    file_hash: 5128c539cd3051e20c09e1924eb0951d5be697be251e10d3c281464ed4c436cd
    line: 737
    column: 3
    function: P0
