- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f79aeccf-7ec2-490a-b231-363d05a056e4
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 751
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= w && w <= 1) && (w == 0 || w == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be19035d-7e49-44cd-a5f9-dfb8f1b96009
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 751
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x && x <= 3) && x <= 127) && x % 3 == 0)
      && (x == 0 || x == 3))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17b93dd0-4e8b-4032-8a48-3f17614e7c84
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 751
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= y && y <= 3) && y <= 127) && y % 3 == 0)
      && (y == 0 || y == 3))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: fdbbbee8-9f5e-4714-9067-5211c2152e07
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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: 21948700-2b6a-4963-9d04-0a38d8ab0fd5
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 737
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c4cdeee6-3d01-450c-ac74-07d3ae2f1fa4
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 741
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bff2c428-b4bf-4a59-9b06-c92ab97f6951
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 742
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1f2b2cc8-afbe-42f9-ba5c-e536452433d9
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 739
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cb201a23-4c38-4bc5-9a37-e1c765c14cb8
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 729
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 65b6b8ba-9223-4844-ab1b-1259c8de65c0
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 714
    column: 3
    function: thr1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 96e535fd-306c-4a13-8347-8a29cc84f9a9
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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: 23308464-256e-4df3-a532-ba433865674c
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 750
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0a46ec29-5682-4fba-a40b-01dd18113d60
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 735
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 756bc01a-f938-45bf-ad86-fc05f0db9f0d
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 710
    column: 1
    function: __VERIFIER_atomic_w
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 101a88b3-9993-49d9-be50-e65fbb55def7
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 734
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b689ac5f-1b05-47c1-b4d3-29682c18597e
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 731
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9857fb6d-9c2c-4c2c-a840-c3f35281fa99
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 716
    column: 3
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 524cef19-c85e-436f-9377-aafa2a8ee1e7
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 728
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a43d6c17-9b93-4212-bff7-e66f0a517a9e
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 719
    column: 1
    function: __VERIFIER_atomic_r
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0e250db-ecef-4150-b12a-7e75cc714ff8
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 723
    column: 1
    function: __VERIFIER_atomic_r
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f3453f80-3fd4-46ec-86ad-16f8ba8291bd
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 732
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8bba074c-7bd4-41be-9ec7-8cff9aa7a801
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 726
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 60ef7084-f369-4c2a-80b5-9e70f03419a5
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 744
    column: 3
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e4fb2a34-0917-4f48-b83e-baa6acdfc35e
    creation_time: 2024-04-30T09:32:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/18_read_write_lock.i: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
      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-ext/18_read_write_lock.i
    file_hash: 72289b7b84ec29dc48aff6fa2f8d521998f594af518139867a01f104107e1865
    line: 705
    column: 1
    function: __VERIFIER_atomic_w
