- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68dcd80a-f801-43fc-840d-a348a2eac81d
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 746
    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: 0b46c2a4-dd7f-493e-a336-ea09b8395f95
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 747
    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: aa9184ce-c226-4f72-8455-912756b58024
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 748
    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: 25f42fe4-6cd5-49d3-9d59-9d3f1669d213
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 749
    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: bd8964aa-907a-422c-ab16-c68588728495
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 746
    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: b7ccf934-80fb-4ca1-9c94-5cdde79ed3cf
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 747
    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: 4bf6d87e-aa81-4e63-b5d9-30dade565544
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 748
    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: acdd23cb-7466-4661-9f09-92a8057da5ed
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 749
    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: 6ff6dea9-38ca-49f2-83f5-28ec21dbb7cf
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 746
    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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b4b8aae-2336-4d21-9f1d-709a30ea604f
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 747
    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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7271cce7-8326-4e28-b328-4fadc33f7a3d
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 748
    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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb7111ba-c4fb-4732-918e-9ee83647b105
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 749
    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: d515bff3-d358-43ad-82e0-6b6c916a2774
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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: 00d62575-a04a-4e3b-baca-f7915f47422a
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 729
    column: 3
    function: reader
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: cbe1b667-63b4-4f86-b792-67150c92b135
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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: 575950be-db04-44e7-a839-fca8a5e21ec6
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 745
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d933876c-1c93-4f33-ad9e-2cf86cf5407b
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 738
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9c6a03a5-0ef0-4768-8196-732eecd2342f
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 735
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1ca7db3f-dd76-42ef-b703-548bfd3b20e3
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 719
    column: 3
    function: writer
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3fa9fbcb-07e0-4118-a1fd-fea92f9720e1
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 733
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e060a80c-ceb7-4342-afa1-5770a205d421
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 715
    column: 1
    function: __VERIFIER_atomic_release_read_lock
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9c77d8d7-98a3-41ca-bcf5-f9eb1342f590
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 713
    column: 1
    function: __VERIFIER_atomic_release_read_lock
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f7f87def-3321-443b-94e5-ca5ce3e7c3ae
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 730
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f885f351-6695-459e-924e-dc5264a9fbfd
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 727
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0dc1a858-5874-47ad-b318-0a6145c48929
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 721
    column: 3
    function: writer
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b1cc1d2-7c22-4fc7-ba88-3e2922fdfdf3
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 732
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 96f4e807-d742-43c2-b4a5-7ef374e36ced
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 712
    column: 1
    function: __VERIFIER_atomic_take_read_lock
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6520b084-1570-4032-aad7-3c8405663110
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 708
    column: 1
    function: __VERIFIER_atomic_take_write_lock
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b6199346-7cbf-4202-ac97-3ab5c92e338e
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 736
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a32b904e-5ae3-4506-a72c-e6dbe2a3807e
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 705
    column: 1
    function: __VERIFIER_atomic_take_write_lock
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1208122a-3fa8-4f1c-a967-36b3859c93d3
    creation_time: 2024-04-30T10:53:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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-atomic/read_write_lock-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1.i: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
      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-atomic/read_write_lock-1.i
    file_hash: 8fab2e995569cc819974baee7d52d8d4bdabd2a2896c83fb3b8d07b44f394c5b
    line: 709
    column: 1
    function: __VERIFIER_atomic_take_read_lock
