- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9e2ec21-bc42-4161-afce-15161d8f4ef6
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 717
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((rwlock.__data.__cur_writer == 0 && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb839817-5a02-4468-a19f-c58754bfe213
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 718
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((rwlock.__data.__cur_writer == 0 && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a03f165b-ccd5-4fb9-85a6-74db4850288e
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 719
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((rwlock.__data.__cur_writer == 0 && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9565526e-767f-4efe-b064-1776b2e1b7d4
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 720
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((rwlock.__data.__cur_writer == 0 && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efc84ad1-269d-4fb8-9531-c349c8c7fdbb
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 717
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((0 <= y
      && y <= 3) && y <= 127) && rwlock.__data.__cur_writer == 0) && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U) && y % 3 == 0) && (y == 0 || y == 3)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 082560f4-9efa-4802-a2fe-e79eb5a361ef
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 718
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((0 <= y
      && y <= 3) && y <= 127) && rwlock.__data.__cur_writer == 0) && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U) && y % 3 == 0) && (y == 0 || y == 3)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddb814c5-5530-4c3d-90f7-32d0f3e75af4
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 719
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((0 <= y
      && y <= 3) && y <= 127) && rwlock.__data.__cur_writer == 0) && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U) && y % 3 == 0) && (y == 0 || y == 3)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: edb57a36-ce0f-408d-b8bd-7c34d9d30fde
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 720
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((0 <= y
      && y <= 3) && y <= 127) && rwlock.__data.__cur_writer == 0) && rwlock.__data.__flags
      == (unsigned char)0) && rwlock.__data.__pad2 == (unsigned char)0) && rwlock.__data.__pad3
      == 0U) && rwlock.__data.__pad4 == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision
      == (signed char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U) && y % 3 == 0) && (y == 0 || y == 3)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8ed6a41-05dc-4060-800b-f71afad9127f
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 717
    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: 40421954-2426-4fef-a268-c3b8aeffba9b
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 718
    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: 40af463e-d5f1-4513-99c4-4c7a3e30663b
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 719
    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: ef9e7129-e1a2-466a-b86d-10021b77f8ab
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 720
    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: 197343e2-1217-483d-adf5-f5c64bf2c307
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 717
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (rwlock_locked || (((((((((((x == 3 && rwlock.__data.__cur_writer
      == 0) && rwlock.__data.__flags == (unsigned char)0) && rwlock.__data.__pad2
      == (unsigned char)0) && rwlock.__data.__pad3 == 0U) && rwlock.__data.__pad4
      == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision == (signed
      char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb338339-8250-4ef1-a574-846306cd6d67
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 718
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (rwlock_locked || (((((((((((x == 3 && rwlock.__data.__cur_writer
      == 0) && rwlock.__data.__flags == (unsigned char)0) && rwlock.__data.__pad2
      == (unsigned char)0) && rwlock.__data.__pad3 == 0U) && rwlock.__data.__pad4
      == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision == (signed
      char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95438459-64ea-4827-906a-f3c9bdd8d8ce
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 719
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (rwlock_locked || (((((((((((x == 3 && rwlock.__data.__cur_writer
      == 0) && rwlock.__data.__flags == (unsigned char)0) && rwlock.__data.__pad2
      == (unsigned char)0) && rwlock.__data.__pad3 == 0U) && rwlock.__data.__pad4
      == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision == (signed
      char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e48ea0e-69b6-4c06-b456-e94e318bb76a
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 720
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (rwlock_locked || (((((((((((x == 3 && rwlock.__data.__cur_writer
      == 0) && rwlock.__data.__flags == (unsigned char)0) && rwlock.__data.__pad2
      == (unsigned char)0) && rwlock.__data.__pad3 == 0U) && rwlock.__data.__pad4
      == 0U) && rwlock.__data.__readers == 0U) && rwlock.__data.__rwelision == (signed
      char)0) && rwlock.__data.__shared == (unsigned char)0) && rwlock.__data.__writers
      == 0U) && rwlock.__data.__writers_futex == 0U) && rwlock.__data.__wrphase_futex
      == 0U))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ccc08530-4e41-4951-88d3-d9a679f0e92d
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 717
    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: 35f484b2-f4a1-495e-86d8-d53a61f84e0f
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 718
    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: f261df3f-4153-4473-80d0-937acec9e529
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 719
    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: b0f5a74c-395f-4199-9f8d-47fb6e5e6b85
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 720
    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: bba95ff0-67aa-4557-abcd-ade618f37c59
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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: 187eb23a-1ddc-412d-b62d-037e9419c56c
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 701
    column: 3
    function: reader
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9809f6fe-a128-4fa6-81bb-5156ee509f25
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: rwlock_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f4a01e1b-079c-4fdd-97e9-972e24c80c69
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: rwlock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 690
    column: 3
    function: writer
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7b6da80d-5a92-467b-a2a3-52624b20bd3d
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 706
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 441a844c-ccf3-4d8f-8af0-b5eca6f377c2
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: rwlock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 711
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 89873431-e271-4a8e-90d7-2f57b861114e
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 704
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a3df6f5d-d552-494f-8227-4071bc45d7a4
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 698
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 248d6d25-bcac-4bf2-bf87-45e9de0670cc
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: rwlock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 692
    column: 3
    function: writer
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cd409ca9-6b64-4967-b498-4962ae9041ee
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 700
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c829244f-f285-475e-9393-e60c26792940
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 707
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 62ccb454-8b05-467e-a136-abc3a48f95dc
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 703
    column: 3
    function: reader
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 0d547da2-4585-4b9d-9a3f-4c6fa091a3ec
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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: a4e45c37-bd62-4152-a8dd-db69bd7fa30a
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 716
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 621e7d83-1457-4632-9c32-9fc5e5937791
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: rwlock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 697
    column: 3
    function: reader
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6678b574-34d1-4262-ba73-350cd571882a
    creation_time: 2024-04-30T09:53:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/read_write_lock-1-pthread.i: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
      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-pthread.i
    file_hash: 04a1d4ff1109dce80fd92bb8b947109ce8379b8f1a452f4ba67af1891a651644
    line: 709
    column: 3
    function: reader
