- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb21c209-5241-44b4-8176-47c503c88a00
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 8f1a7566-0a45-4bd2-8c10-9a62b1cbd983
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 11905b2e-eeb7-49e7-904c-c9061256b466
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 391e3af1-bfe6-4a6f-8934-ec1b35eda775
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 8035498d-f784-4d65-96f7-fceffdcc1e56
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 228020fc-2bb7-45b5-9535-c4a60d04c8b7
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 171d4913-d55c-4180-aa4b-15e6f0ea078a
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: fd387090-16be-42b7-97f6-996faa582fa8
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: e04c61e2-7461-491b-a5a8-278205bc14da
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 1e011ba6-027e-401d-8bdc-0bca88fbe110
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 65be5de7-728a-49e8-9479-d5c701434b99
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: c177333d-d261-48b0-86a2-fe93398c300e
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 50d2e07a-278e-4fe7-9de5-f6eafce0a774
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 101abb1f-2728-457f-9363-87c208f01111
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 950f82a1-f89f-4214-b7fa-7a09dad8e6de
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 58b6a5dc-4c90-48d2-b21d-779f93e99ac3
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 94c1290e-8f1c-4b28-aacf-4f166943cfe2
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 2512de15-c9db-42e4-a0e8-5327324920ee
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: ab391d78-820c-4e83-8772-75d5fbbd6573
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: ee8b8fbd-dd33-42c5-a632-87c91a584508
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 7f6b625a-ce71-435a-ae38-6a55ac6442e4
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 337f7328-2432-4821-9d2b-5b2bfa4e8eb5
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: dbdca7eb-742e-46fa-b9fb-5b1ec3d600c0
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 95b3f083-343e-414e-93b7-c58f6ab3879a
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: ea67567f-e294-473c-bcb1-454e0d36f28f
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 94836dfd-4a6f-483c-b3c1-540e23747664
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 40fceb59-be6e-49ac-abf7-944a7af2a87b
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 09603d75-0b87-4e89-b763-2de3d14218b3
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: f1f28a3c-f030-457b-8188-86a176be072d
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 89b78c0e-71a3-409a-b33b-62a0b6a99db0
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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: 23b67d61-674c-4add-9be1-3e6eff1dccfa
    creation_time: 2024-04-30T11:24:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-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
