- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b66b70e8-2d75-4bec-b38b-36e308e663af
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 690f9526-3ece-4287-b507-6ac4e9ad2c44
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: d70a4c25-51af-4826-916d-5ae91f5260fe
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: ceaed6bd-849b-480d-a8cf-ea34ba8ba672
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: d5dd86c4-a60f-4c8c-b320-6987107d64be
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 5d747e42-638e-4b71-bcf5-2ae0561f2dda
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 6261afa2-388c-4ef6-98bc-4d22265f15d4
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: c4526526-fb99-45bb-baa9-d3988b9cf0b3
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc873415-9619-4372-88a4-4e753a6b5419
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 2604d756-57f2-4c8b-ab53-308ea947dda4
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 564632ce-7d77-4459-b8fe-1ca5528014f4
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 202ae942-a2f3-4537-8eef-c458fe105306
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: a8e93ca1-9f7d-4f3f-a340-f6d5a6fb616a
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: e3de49f5-a314-4154-9668-f4a7c925178a
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: bc621375-0cd0-422e-ac65-04b05eda30ad
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 27f72ee8-aae6-4feb-b077-5b2664adf767
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 8055b7d5-6275-4f3c-be5f-4172152459d2
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 1af2b5f7-7463-4e6b-b948-63c3a25ff4e2
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 86f35deb-74a6-442d-88a9-0396cadb2f58
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 7d166526-f534-4603-83a3-6b0e063ddf7f
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 7ebd4b96-fe85-462f-8ada-6729a73dea4f
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: a71cea2e-9d1e-4b20-a5e8-4874fe3f67f7
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: c8b49d4f-fb3b-4768-b03e-86d06efeed60
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: f2e37c8c-7751-40a2-b45e-86d1e8b3c5aa
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: d908b627-d824-49ee-b535-a4b359fc1f5a
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 28f51acf-b115-4c70-bc48-074b51fd96c4
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: dacf411a-1d44-4981-95a9-b2fc22348b5f
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 0bcacfea-fdd4-40d3-b2f2-a04ce44d979d
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 0fa0aa53-1bd7-4843-b3f7-f05138322147
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: 57839fd5-1ee5-4279-acff-0e0fa6ef703f
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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: c301aaed-6c71-4efc-8495-5f8d135a6a12
    creation_time: 2024-04-25T07:32:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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
