- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46cc7877-1fd3-4a8c-838c-f1dfcaee6039
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    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: d6da1617-9ac7-43b8-8dad-967ca3cb1074
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    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: e7d66f1c-41eb-489e-881b-9a65d73a9b91
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || jiffies == 0UL'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4c3c4e0-d1a5-4091-abe5-8e4adf92734a
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || jiffies == 0UL'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82dd2bde-c4f5-4aba-857e-8885a6d9f617
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((_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: b59d1dd9-4b88-4525-9795-568b329f5537
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((_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: e1d825b5-f667-4203-91fe-40aa799d55cd
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    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: 3d125175-d8a9-4f5d-a24e-f4d9cf335941
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    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: b4ae18f6-b0b0-44bc-8b17-f68b11ce8df5
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    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: 8ef6037c-263f-47d4-91c0-15b363777d2f
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    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: afce95c4-f415-4f03-9149-40e6362c009e
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6862
    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: 4be46c1f-bdf0-4966-b9d8-79fb5f45fe6b
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6863
    column: 2
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((nvram_fops.check_flags ==
      0 && nvram_fops.compat_ioctl == 0) && nvram_fops.dir_notify == 0) && nvram_fops.fasync
      == 0) && nvram_fops.flock == 0) && nvram_fops.flush == 0) && nvram_fops.fsync
      == 0) && nvram_fops.get_unmapped_area == 0) && nvram_fops.ioctl == 0) && nvram_fops.llseek
      == & nvram_llseek) && nvram_fops.lock == 0) && nvram_fops.mmap == 0) && nvram_fops.open
      == 0) && nvram_fops.open_exec == 0) && nvram_fops.owner == 0) && nvram_fops.poll
      == 0) && nvram_fops.read == & read_nvram) && nvram_fops.readdir == 0) && nvram_fops.readv
      == 0) && nvram_fops.release == 0) && nvram_fops.sendfile == 0) && nvram_fops.sendpage
      == 0) && nvram_fops.unlocked_ioctl == & nvram_unlocked_ioctl) && nvram_fops.write
      == & write_nvram) && nvram_fops.writev == 0)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 2c1259f7-72ed-4a73-bfa4-fe66a10cafed
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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: 39a4cb4d-533c-470f-a8f4-43da252f7761
    creation_time: 2024-06-19T11:50:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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_nvram_unlocked_ioctl_write_nvram.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-driver-races/char_generic_nvram_nvram_unlocked_ioctl_write_nvram.i: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
      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_nvram_unlocked_ioctl_write_nvram.i
    file_hash: 1941de74eb261e3f3ecbbb76e1746df74b536a1b8190d4ca9fd6a4341892fdcb
    line: 6861
    column: 2
    function: main
