- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04f02ede-0235-4d44-b8fb-05afd0688a36
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 759
    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: 664cfa84-b2d8-41cd-acdb-138731121867
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 760
    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: 66f1d0e2-3571-42ca-acfd-c0df7502f289
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 759
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((0 <= __unbuffered_cnt
      && 0 <= x) && 0 <= y) && x <= 2) && y <= 2) && y <= 127) && ((x == 0 || x ==
      1) || x == 2)) && ((y == 0 || y == 1) || y == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97769706-3a1e-4f6d-ae62-51829fb61454
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 760
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((0 <= __unbuffered_cnt
      && 0 <= x) && 0 <= y) && x <= 2) && y <= 2) && y <= 127) && ((x == 0 || x ==
      1) || x == 2)) && ((y == 0 || y == 1) || y == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffc0dc57-b9c7-4a00-b441-600db0efbd8c
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 759
    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: 1c088ce0-c4e2-4882-86e5-1ce7da869026
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 760
    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: 3c755f85-c416-48a7-aae1-3ca10e81c8e4
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 759
    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: d201a2a2-f2a2-487a-85c0-6276054cd00d
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 760
    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: afd1f8a0-7b83-4e05-a4fb-ccd868403a67
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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: b60e7f83-703a-4287-be3a-6ca18a76bb0e
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 764
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf7c35f4-0ac1-4238-90c0-e82ab6858011
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 765
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 41d606bd-3713-497e-a5f0-633f36655f8f
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 737
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2028df10-c846-4b9d-b6b1-9a88ea5b5417
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 760
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5af45b58-414c-41a6-8cec-fdf1ce69fa9a
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 727
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 57470200-528a-4ed4-8d32-e04d59a47c9d
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 722
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed226fbe-5213-479b-bce7-8d619834be69
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 723
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6180c037-1c94-4dba-a5e1-76e1ff4c9144
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 742
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6da5c601-5319-400c-9b30-5f64cd634216
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 719
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0cc07ded-4dfb-4bd6-b362-6407e25be0a5
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 739
    column: 3
    function: P1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 115eb467-d5fe-4a56-b00e-8224bade2e61
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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: 611f061f-e6f3-418f-8e04-2f8e87ede820
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 757
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 22d38262-9a08-4c42-a399-9cd198aa8d76
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 720
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 14147bb3-e101-4a26-8639-7004293b0eee
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 735
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 77d25479-6a86-445e-ae3c-8bf6222f94bc
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 724
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a81ae3a-390f-4cca-9a40-e50bca7bda18
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 768
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8af8eb7e-e979-4601-baf0-8350f34e398a
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 717
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b08ac7ef-95a1-414e-86e8-e6ceebc6e9de
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 738
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dbfe7ebb-9908-4dd9-bd86-29c97ff67764
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 762
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 310b9bb4-7234-428d-86a0-ef44fe52f4f1
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 740
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 89f5ada5-6956-4963-9189-4d7f33ab80b1
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 732
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 74f87e17-8653-45e4-a014-c76fb69f9464
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 734
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 052b66a4-17b4-4b59-a1f1-ab4cdf52822d
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 766
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e78a3b32-5689-42d9-afe1-81a715a451f5
    creation_time: 2024-04-30T11:22:50Z
    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/safe029_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe029_tso.i: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
      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/safe029_tso.i
    file_hash: ef851e22a0a98929f1b90876fcac5ec793e10efa4691f239ca948c8dc39b94fd
    line: 725
    column: 3
    function: P0
