- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ade90a7-2189-4443-9087-5fc2a2941ac5
    creation_time: 2024-04-30T10:04:00Z
    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-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 || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((_whoop_init
      == & nvram_init && _whoop_exit == & nvram_cleanup) && jiffies == 0UL) && 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) && (unsigned int )default_alloc_size
      == 4U))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 209d68fb-4458-4a78-812a-9a75249a93d4
    creation_time: 2024-04-30T10:04:00Z
    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-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 || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((_whoop_init
      == & nvram_init && _whoop_exit == & nvram_cleanup) && jiffies == 0UL) && 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) && (unsigned int )default_alloc_size
      == 4U))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14e1575c-6f71-4e39-8366-693bff3df4bb
    creation_time: 2024-04-30T10:04:00Z
    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-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: bb21ed45-214d-4c48-a25d-1b00ab140ff1
    creation_time: 2024-04-30T10:04:00Z
    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-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: ef6b1c8e-12d6-429f-99cf-1059a99eee0d
    creation_time: 2024-04-30T10:04:00Z
    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-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: e21fae4b-9077-4a8e-9061-47e6d55cf6d8
    creation_time: 2024-04-30T10:04:00Z
    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-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: 310dec54-a5be-4a43-8bea-86a9008ef523
    creation_time: 2024-04-30T10:04:00Z
    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-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: 5e7eec0e-b7f2-4896-8581-f58ae0196fc7
    creation_time: 2024-04-30T10:04:00Z
    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-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: ec86c81d-ecf2-469a-be09-f5b2c401ec18
    creation_time: 2024-04-30T10:04:00Z
    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-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: 7d294be3-2576-4bef-8f92-6a908445a1b5
    creation_time: 2024-04-30T10:04:00Z
    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-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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9351f011-c196-4b2e-a3f6-c08c3861335f
    creation_time: 2024-04-30T10:04:00Z
    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-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: 52ec3687-4137-4496-aa17-d75704dcef9a
    creation_time: 2024-04-30T10:04:00Z
    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-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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 3476741f-5244-42cc-9ccf-58b70e213bd5
    creation_time: 2024-04-30T10:04:00Z
    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-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: 0d0502b9-ed5d-4746-ac1d-5cb780336d9c
    creation_time: 2024-04-30T10:04:00Z
    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-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: e284cd0c-3c21-4076-94f5-86423c097192
    creation_time: 2024-04-30T10:04:00Z
    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-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: 5d6c41ab-91f5-46cd-8f2b-be4918653c28
    creation_time: 2024-04-30T10:04:00Z
    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-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: 305c2013-f1f4-413e-a6f7-52f5e15da199
    creation_time: 2024-04-30T10:04:00Z
    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-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: e8c5fa22-0f46-4e2f-bf3b-8004ce535c6a
    creation_time: 2024-04-30T10:04:00Z
    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-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: 4b07c5ee-4564-4b4b-b332-e2fb2de8709b
    creation_time: 2024-04-30T10:04:00Z
    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-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: c687e16b-be85-456d-b361-4e7d3adf70ed
    creation_time: 2024-04-30T10:04:00Z
    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-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: 59bfd38f-0436-4c8d-8b3a-03f8ab5cd397
    creation_time: 2024-04-30T10:04:00Z
    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-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: e93fc725-e92c-4580-8768-4251feff8c3f
    creation_time: 2024-04-30T10:04:00Z
    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-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: 55800f14-b548-4512-bd92-bfb911c1ab10
    creation_time: 2024-04-30T10:04:00Z
    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-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: b9121d86-ce19-45bf-9b3f-b69c08575716
    creation_time: 2024-04-30T10:04:00Z
    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-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: 31df611f-57b4-486a-97e2-6b428ffc6665
    creation_time: 2024-04-30T10:04:00Z
    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-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: 617cc849-87dc-439c-b2ff-0b5ee62c915e
    creation_time: 2024-04-30T10:04:00Z
    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-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: 9c0c049a-1439-4e0d-87d3-e62db73f3569
    creation_time: 2024-04-30T10:04:00Z
    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-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: bb1a887b-ef79-490f-939a-5f26f40f4fde
    creation_time: 2024-04-30T10:04:00Z
    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-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: c5483ead-9a45-4854-b985-fc292c2d48d4
    creation_time: 2024-04-30T10:04:00Z
    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-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: 5e634b2c-711a-46d3-9d48-3797059c2cca
    creation_time: 2024-04-30T10:04:00Z
    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-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
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 683941bc-e0ad-4d3b-9b61-e07b17ea4af3
    creation_time: 2024-04-30T10:04:00Z
    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-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
