- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f2dfb4e-df39-457a-b21d-73425c0144e6
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6884
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || (unsigned int )default_alloc_size == 4U'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d942d4ed-206f-4d70-86e1-a26ecec71901
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6885
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || (unsigned int )default_alloc_size == 4U'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2741c9a3-8b5d-4eb1-a3ca-9101c39bf6e1
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6884
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_exit == & nvram_cleanup'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9542a6df-8b94-4b92-9f59-f8e4f9591919
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6885
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_exit == & nvram_cleanup'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7e04302-3fdf-43f2-91c2-cdc2870a51ee
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6884
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || jiffies == 0UL'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d758c8d-5ecc-4e65-85b5-2665c7184e2d
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6885
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || jiffies == 0UL'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df79c687-9e86-4206-bc15-e55babafce8a
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6884
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_init == & nvram_init'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d41762a-a4a3-4b4b-a244-c3251d90df83
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6885
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || _whoop_init == & nvram_init'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ef60d0f-1cc6-434d-a936-fce03a60265a
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6884
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((nvram_fops.check_flags ==
      0 && nvram_fops.compat_ioctl == 0) && nvram_fops.dir_notify == 0) && nvram_fops.fasync
      == 0) && nvram_fops.flock == 0) && nvram_fops.flush == 0) && nvram_fops.fsync
      == 0) && nvram_fops.get_unmapped_area == 0) && nvram_fops.ioctl == 0) && nvram_fops.llseek
      == & nvram_llseek) && nvram_fops.lock == 0) && nvram_fops.mmap == 0) && nvram_fops.open
      == 0) && nvram_fops.open_exec == 0) && nvram_fops.owner == 0) && nvram_fops.poll
      == 0) && nvram_fops.read == & read_nvram) && nvram_fops.readdir == 0) && nvram_fops.readv
      == 0) && nvram_fops.release == 0) && nvram_fops.sendfile == 0) && nvram_fops.sendpage
      == 0) && nvram_fops.unlocked_ioctl == & nvram_unlocked_ioctl) && nvram_fops.write
      == & write_nvram) && nvram_fops.writev == 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a58885d-055e-4925-99d1-fe2548467b25
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6885
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((nvram_fops.check_flags ==
      0 && nvram_fops.compat_ioctl == 0) && nvram_fops.dir_notify == 0) && nvram_fops.fasync
      == 0) && nvram_fops.flock == 0) && nvram_fops.flush == 0) && nvram_fops.fsync
      == 0) && nvram_fops.get_unmapped_area == 0) && nvram_fops.ioctl == 0) && nvram_fops.llseek
      == & nvram_llseek) && nvram_fops.lock == 0) && nvram_fops.mmap == 0) && nvram_fops.open
      == 0) && nvram_fops.open_exec == 0) && nvram_fops.owner == 0) && nvram_fops.poll
      == 0) && nvram_fops.read == & read_nvram) && nvram_fops.readdir == 0) && nvram_fops.readv
      == 0) && nvram_fops.release == 0) && nvram_fops.sendfile == 0) && nvram_fops.sendpage
      == 0) && nvram_fops.unlocked_ioctl == & nvram_unlocked_ioctl) && nvram_fops.write
      == & write_nvram) && nvram_fops.writev == 0)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7aa91673-984f-41e1-9f0d-82ca0210cb62
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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: cb1b3ca1-54c6-4ff0-817b-3faa1128b2ad
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6717
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 09cc0229-cdd3-48ca-8f6e-354c075f13ff
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6750
    column: 2
    function: write_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0e3bae7d-9767-4657-9bc8-2bfc58097736
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6726
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9cdc9359-bac2-45b9-8c69-ab3e27ef7e9c
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6729
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d3a28e1f-e8c8-4082-9203-d0bba9958761
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6743
    column: 2
    function: write_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 56fdca89-d3fd-4a6b-85a5-e933cb3bc0bb
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6715
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42a0967b-77c9-474f-be3a-ec1e4d58b3d3
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6722
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9d2d4a2c-2531-45c4-b45d-87de3326a3fd
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6748
    column: 2
    function: write_nvram
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 999c77ec-ee1c-4d25-b294-2b77acaa54f4
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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: 55f0a45a-05ae-4c5a-a121-74bc7a8461fb
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6883
    column: 2
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3f721092-b467-458d-9556-c27fd7a543b4
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6731
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: acf39b5d-f949-4d9b-8278-d2af1b8c9589
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6745
    column: 2
    function: write_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 90464fbb-dfd8-4b4f-af89-d0c98012c0fd
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6756
    column: 2
    function: write_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7b6464ad-2e5a-46a7-b637-6e063d1ace73
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6758
    column: 2
    function: write_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 94e4988e-e2b8-4499-af8d-7509257df90f
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6761
    column: 2
    function: write_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9a00ec2c-53d5-4ae8-b738-b85734e2b67c
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6720
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 65f57f22-b591-4e8d-abee-7365640a1385
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6728
    column: 2
    function: read_nvram
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6125fbc8-540e-49d2-8776-bfdaecdc4c8d
    creation_time: 2024-04-29T11:02:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
      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-driver-races/char_generic_nvram_read_nvram_write_nvram.i
    file_hash: e2e7bb75a4a041a1b509d755288a88858836cab5db2230ae4fd0db7ec04fe254
    line: 6759
    column: 2
    function: write_nvram
