- entry_type: ghost_instrumentation
  metadata:
    format_version: "2.0"
    uuid: 3afbb805-e4ec-497c-b7a3-fb1c6c26e201
    creation_time: 2025-05-28T12:15:02Z
    producer:
      name: Goblint
      version: heads/master-0-gb8fb60e5d-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  content:
    ghost_variables:
    - name: multithreaded
      scope: global
      type: int
      initial:
        value: "0"
        format: c_expression
    - name: smutex_lock_of_w83977af_ir_locked
      scope: global
      type: int
      initial:
        value: "0"
        format: c_expression
    ghost_updates:
    - location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 9420
        column: 3
        function: ldv_spin_unlock_lock_of_w83977af_ir
      updates:
      - variable: smutex_lock_of_w83977af_ir_locked
        value: "0"
        format: c_expression
    - location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 9411
        column: 3
        function: ldv_spin_lock_lock_of_w83977af_ir
      updates:
      - variable: smutex_lock_of_w83977af_ir_locked
        value: "1"
        format: c_expression
    - location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7628
        column: 3
        function: ldv_dispatch_insmod_register_10_3
      updates:
      - variable: multithreaded
        value: "1"
        format: c_expression
- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 156ac412-3860-4648-9a27-31b238bbf7e7
    creation_time: 2025-05-28T12:15:02Z
    producer:
      name: Goblint
      version: heads/master-0-gb8fb60e5d-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  content:
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7630
        column: 3
        function: ldv_dispatch_insmod_register_10_3
      value: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((x86_dma_fallback_dev.coherent_dma_mask
        & 0ULL) == 0ULL && (x86_dma_fallback_dev.devt & 0U) == 0U) && (x86_dma_fallback_dev.id
        & 0U) == 0U) && (x86_dma_fallback_dev.kobj.release.timer.data & 0UL) == 0UL)
        && (x86_dma_fallback_dev.kobj.release.timer.expires & 0UL) == 0UL) && (x86_dma_fallback_dev.kobj.release.timer.lockdep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.kobj.release.work.lockdep_map.ip &
        0UL) == 0UL) && (x86_dma_fallback_dev.kobj.state_add_uevent_sent & 0U) ==
        0U) && (x86_dma_fallback_dev.kobj.state_in_sysfs & 0U) == 0U) && (x86_dma_fallback_dev.kobj.state_initialized
        & 0U) == 0U) && (x86_dma_fallback_dev.kobj.state_remove_uevent_sent & 0U)
        == 0U) && (x86_dma_fallback_dev.kobj.uevent_suppress & 0U) == 0U) && (x86_dma_fallback_dev.mutex.dep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.accounting_timestamp & 0UL)
        == 0UL) && (x86_dma_fallback_dev.power.active_jiffies & 0UL) == 0UL) && (x86_dma_fallback_dev.power.async_suspend
        & 0U) == 0U) && (x86_dma_fallback_dev.power.can_wakeup & 0U) == 0U) && (x86_dma_fallback_dev.power.completion.done
        & 0U) == 0U) && (x86_dma_fallback_dev.power.deferred_resume & 0U) == 0U) &&
        (x86_dma_fallback_dev.power.disable_depth & 0U) == 0U) && (x86_dma_fallback_dev.power.idle_notification
        & 0U) == 0U) && (x86_dma_fallback_dev.power.irq_safe & 0U) == 0U) && (x86_dma_fallback_dev.power.last_busy
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.memalloc_noio & 0U) == 0U) &&
        (x86_dma_fallback_dev.power.no_callbacks & 0U) == 0U) && (x86_dma_fallback_dev.power.request_pending
        & 0U) == 0U) && (x86_dma_fallback_dev.power.run_wake & 0U) == 0U) && (x86_dma_fallback_dev.power.runtime_auto
        & 0U) == 0U) && (x86_dma_fallback_dev.power.suspend_timer.data & 0UL) == 0UL)
        && (x86_dma_fallback_dev.power.suspend_timer.expires & 0UL) == 0UL) && (x86_dma_fallback_dev.power.suspend_timer.lockdep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.suspended_jiffies & 0UL) ==
        0UL) && (x86_dma_fallback_dev.power.timer_autosuspends & 0U) == 0U) && (x86_dma_fallback_dev.power.timer_expires
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.use_autosuspend & 0U) == 0U)
        && (x86_dma_fallback_dev.power.work.lockdep_map.ip & 0UL) == 0UL) && (~ x86_dma_fallback_dev.coherent_dma_mask
        & 0ULL) == 0ULL) && (~ x86_dma_fallback_dev.devt & 0U) == 0U) && (~ x86_dma_fallback_dev.id
        & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.release.timer.data & 0UL) ==
        0UL) && (~ x86_dma_fallback_dev.kobj.release.timer.expires & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.release.timer.lockdep_map.ip & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.release.work.lockdep_map.ip & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.state_add_uevent_sent & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.state_in_sysfs
        & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.state_initialized & 0U) == 0U)
        && (~ x86_dma_fallback_dev.kobj.state_remove_uevent_sent & 0U) == 0U) && (~
        x86_dma_fallback_dev.kobj.uevent_suppress & 0U) == 0U) && (~ x86_dma_fallback_dev.mutex.dep_map.ip
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.accounting_timestamp & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.active_jiffies & 0UL) == 0UL) &&
        (~ x86_dma_fallback_dev.power.async_suspend & 0U) == 0U) && (~ x86_dma_fallback_dev.power.can_wakeup
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.completion.done & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.deferred_resume & 0U) == 0U) && (~ x86_dma_fallback_dev.power.disable_depth
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.idle_notification & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.irq_safe & 0U) == 0U) && (~ x86_dma_fallback_dev.power.last_busy
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.memalloc_noio & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.no_callbacks & 0U) == 0U) && (~ x86_dma_fallback_dev.power.request_pending
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.run_wake & 0U) == 0U) && (~
        x86_dma_fallback_dev.power.runtime_auto & 0U) == 0U) && (~ x86_dma_fallback_dev.power.suspend_timer.data
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.suspend_timer.expires & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.suspend_timer.lockdep_map.ip & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.suspended_jiffies & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.power.timer_autosuspends & 0U) == 0U) && (~ x86_dma_fallback_dev.power.timer_expires
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.use_autosuspend & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.work.lockdep_map.ip & 0UL) == 0UL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7662
        column: 3
        function: ldv_dispatch_irq_register_8_3
      value: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((x86_dma_fallback_dev.coherent_dma_mask
        & 0ULL) == 0ULL && (x86_dma_fallback_dev.devt & 0U) == 0U) && (x86_dma_fallback_dev.id
        & 0U) == 0U) && (x86_dma_fallback_dev.kobj.release.timer.data & 0UL) == 0UL)
        && (x86_dma_fallback_dev.kobj.release.timer.expires & 0UL) == 0UL) && (x86_dma_fallback_dev.kobj.release.timer.lockdep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.kobj.release.work.lockdep_map.ip &
        0UL) == 0UL) && (x86_dma_fallback_dev.kobj.state_add_uevent_sent & 0U) ==
        0U) && (x86_dma_fallback_dev.kobj.state_in_sysfs & 0U) == 0U) && (x86_dma_fallback_dev.kobj.state_initialized
        & 0U) == 0U) && (x86_dma_fallback_dev.kobj.state_remove_uevent_sent & 0U)
        == 0U) && (x86_dma_fallback_dev.kobj.uevent_suppress & 0U) == 0U) && (x86_dma_fallback_dev.mutex.dep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.accounting_timestamp & 0UL)
        == 0UL) && (x86_dma_fallback_dev.power.active_jiffies & 0UL) == 0UL) && (x86_dma_fallback_dev.power.async_suspend
        & 0U) == 0U) && (x86_dma_fallback_dev.power.can_wakeup & 0U) == 0U) && (x86_dma_fallback_dev.power.completion.done
        & 0U) == 0U) && (x86_dma_fallback_dev.power.deferred_resume & 0U) == 0U) &&
        (x86_dma_fallback_dev.power.disable_depth & 0U) == 0U) && (x86_dma_fallback_dev.power.idle_notification
        & 0U) == 0U) && (x86_dma_fallback_dev.power.irq_safe & 0U) == 0U) && (x86_dma_fallback_dev.power.last_busy
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.memalloc_noio & 0U) == 0U) &&
        (x86_dma_fallback_dev.power.no_callbacks & 0U) == 0U) && (x86_dma_fallback_dev.power.request_pending
        & 0U) == 0U) && (x86_dma_fallback_dev.power.run_wake & 0U) == 0U) && (x86_dma_fallback_dev.power.runtime_auto
        & 0U) == 0U) && (x86_dma_fallback_dev.power.suspend_timer.data & 0UL) == 0UL)
        && (x86_dma_fallback_dev.power.suspend_timer.expires & 0UL) == 0UL) && (x86_dma_fallback_dev.power.suspend_timer.lockdep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.suspended_jiffies & 0UL) ==
        0UL) && (x86_dma_fallback_dev.power.timer_autosuspends & 0U) == 0U) && (x86_dma_fallback_dev.power.timer_expires
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.use_autosuspend & 0U) == 0U)
        && (x86_dma_fallback_dev.power.work.lockdep_map.ip & 0UL) == 0UL) && (~ x86_dma_fallback_dev.coherent_dma_mask
        & 0ULL) == 0ULL) && (~ x86_dma_fallback_dev.devt & 0U) == 0U) && (~ x86_dma_fallback_dev.id
        & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.release.timer.data & 0UL) ==
        0UL) && (~ x86_dma_fallback_dev.kobj.release.timer.expires & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.release.timer.lockdep_map.ip & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.release.work.lockdep_map.ip & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.state_add_uevent_sent & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.state_in_sysfs
        & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.state_initialized & 0U) == 0U)
        && (~ x86_dma_fallback_dev.kobj.state_remove_uevent_sent & 0U) == 0U) && (~
        x86_dma_fallback_dev.kobj.uevent_suppress & 0U) == 0U) && (~ x86_dma_fallback_dev.mutex.dep_map.ip
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.accounting_timestamp & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.active_jiffies & 0UL) == 0UL) &&
        (~ x86_dma_fallback_dev.power.async_suspend & 0U) == 0U) && (~ x86_dma_fallback_dev.power.can_wakeup
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.completion.done & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.deferred_resume & 0U) == 0U) && (~ x86_dma_fallback_dev.power.disable_depth
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.idle_notification & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.irq_safe & 0U) == 0U) && (~ x86_dma_fallback_dev.power.last_busy
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.memalloc_noio & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.no_callbacks & 0U) == 0U) && (~ x86_dma_fallback_dev.power.request_pending
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.run_wake & 0U) == 0U) && (~
        x86_dma_fallback_dev.power.runtime_auto & 0U) == 0U) && (~ x86_dma_fallback_dev.power.suspend_timer.data
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.suspend_timer.expires & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.suspend_timer.lockdep_map.ip & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.suspended_jiffies & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.power.timer_autosuspends & 0U) == 0U) && (~ x86_dma_fallback_dev.power.timer_expires
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.use_autosuspend & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.work.lockdep_map.ip & 0UL) == 0UL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7679
        column: 3
        function: ldv_dispatch_register_7_4
      value: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((x86_dma_fallback_dev.coherent_dma_mask
        & 0ULL) == 0ULL && (x86_dma_fallback_dev.devt & 0U) == 0U) && (x86_dma_fallback_dev.id
        & 0U) == 0U) && (x86_dma_fallback_dev.kobj.release.timer.data & 0UL) == 0UL)
        && (x86_dma_fallback_dev.kobj.release.timer.expires & 0UL) == 0UL) && (x86_dma_fallback_dev.kobj.release.timer.lockdep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.kobj.release.work.lockdep_map.ip &
        0UL) == 0UL) && (x86_dma_fallback_dev.kobj.state_add_uevent_sent & 0U) ==
        0U) && (x86_dma_fallback_dev.kobj.state_in_sysfs & 0U) == 0U) && (x86_dma_fallback_dev.kobj.state_initialized
        & 0U) == 0U) && (x86_dma_fallback_dev.kobj.state_remove_uevent_sent & 0U)
        == 0U) && (x86_dma_fallback_dev.kobj.uevent_suppress & 0U) == 0U) && (x86_dma_fallback_dev.mutex.dep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.accounting_timestamp & 0UL)
        == 0UL) && (x86_dma_fallback_dev.power.active_jiffies & 0UL) == 0UL) && (x86_dma_fallback_dev.power.async_suspend
        & 0U) == 0U) && (x86_dma_fallback_dev.power.can_wakeup & 0U) == 0U) && (x86_dma_fallback_dev.power.completion.done
        & 0U) == 0U) && (x86_dma_fallback_dev.power.deferred_resume & 0U) == 0U) &&
        (x86_dma_fallback_dev.power.disable_depth & 0U) == 0U) && (x86_dma_fallback_dev.power.idle_notification
        & 0U) == 0U) && (x86_dma_fallback_dev.power.irq_safe & 0U) == 0U) && (x86_dma_fallback_dev.power.last_busy
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.memalloc_noio & 0U) == 0U) &&
        (x86_dma_fallback_dev.power.no_callbacks & 0U) == 0U) && (x86_dma_fallback_dev.power.request_pending
        & 0U) == 0U) && (x86_dma_fallback_dev.power.run_wake & 0U) == 0U) && (x86_dma_fallback_dev.power.runtime_auto
        & 0U) == 0U) && (x86_dma_fallback_dev.power.suspend_timer.data & 0UL) == 0UL)
        && (x86_dma_fallback_dev.power.suspend_timer.expires & 0UL) == 0UL) && (x86_dma_fallback_dev.power.suspend_timer.lockdep_map.ip
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.suspended_jiffies & 0UL) ==
        0UL) && (x86_dma_fallback_dev.power.timer_autosuspends & 0U) == 0U) && (x86_dma_fallback_dev.power.timer_expires
        & 0UL) == 0UL) && (x86_dma_fallback_dev.power.use_autosuspend & 0U) == 0U)
        && (x86_dma_fallback_dev.power.work.lockdep_map.ip & 0UL) == 0UL) && (~ x86_dma_fallback_dev.coherent_dma_mask
        & 0ULL) == 0ULL) && (~ x86_dma_fallback_dev.devt & 0U) == 0U) && (~ x86_dma_fallback_dev.id
        & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.release.timer.data & 0UL) ==
        0UL) && (~ x86_dma_fallback_dev.kobj.release.timer.expires & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.release.timer.lockdep_map.ip & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.release.work.lockdep_map.ip & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.kobj.state_add_uevent_sent & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.state_in_sysfs
        & 0U) == 0U) && (~ x86_dma_fallback_dev.kobj.state_initialized & 0U) == 0U)
        && (~ x86_dma_fallback_dev.kobj.state_remove_uevent_sent & 0U) == 0U) && (~
        x86_dma_fallback_dev.kobj.uevent_suppress & 0U) == 0U) && (~ x86_dma_fallback_dev.mutex.dep_map.ip
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.accounting_timestamp & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.active_jiffies & 0UL) == 0UL) &&
        (~ x86_dma_fallback_dev.power.async_suspend & 0U) == 0U) && (~ x86_dma_fallback_dev.power.can_wakeup
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.completion.done & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.deferred_resume & 0U) == 0U) && (~ x86_dma_fallback_dev.power.disable_depth
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.idle_notification & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.irq_safe & 0U) == 0U) && (~ x86_dma_fallback_dev.power.last_busy
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.memalloc_noio & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.no_callbacks & 0U) == 0U) && (~ x86_dma_fallback_dev.power.request_pending
        & 0U) == 0U) && (~ x86_dma_fallback_dev.power.run_wake & 0U) == 0U) && (~
        x86_dma_fallback_dev.power.runtime_auto & 0U) == 0U) && (~ x86_dma_fallback_dev.power.suspend_timer.data
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.suspend_timer.expires & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.suspend_timer.lockdep_map.ip & 0UL)
        == 0UL) && (~ x86_dma_fallback_dev.power.suspended_jiffies & 0UL) == 0UL)
        && (~ x86_dma_fallback_dev.power.timer_autosuspends & 0U) == 0U) && (~ x86_dma_fallback_dev.power.timer_expires
        & 0UL) == 0UL) && (~ x86_dma_fallback_dev.power.use_autosuspend & 0U) == 0U)
        && (~ x86_dma_fallback_dev.power.work.lockdep_map.ip & 0UL) == 0UL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7630
        column: 3
        function: ldv_dispatch_insmod_register_10_3
      value: '! multithreaded || ((((((ioport_resource.end & 0ULL) == 0ULL && (ioport_resource.flags
        & 0UL) == 0UL) && (ioport_resource.start & 0ULL) == 0ULL) && (~ ioport_resource.end
        & 0ULL) == 0ULL) && (~ ioport_resource.flags & 0UL) == 0UL) && (~ ioport_resource.start
        & 0ULL) == 0ULL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7662
        column: 3
        function: ldv_dispatch_irq_register_8_3
      value: '! multithreaded || ((((((ioport_resource.end & 0ULL) == 0ULL && (ioport_resource.flags
        & 0UL) == 0UL) && (ioport_resource.start & 0ULL) == 0ULL) && (~ ioport_resource.end
        & 0ULL) == 0ULL) && (~ ioport_resource.flags & 0UL) == 0UL) && (~ ioport_resource.start
        & 0ULL) == 0ULL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7679
        column: 3
        function: ldv_dispatch_register_7_4
      value: '! multithreaded || ((((((ioport_resource.end & 0ULL) == 0ULL && (ioport_resource.flags
        & 0UL) == 0UL) && (ioport_resource.start & 0ULL) == 0ULL) && (~ ioport_resource.end
        & 0ULL) == 0ULL) && (~ ioport_resource.flags & 0UL) == 0UL) && (~ ioport_resource.start
        & 0ULL) == 0ULL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7630
        column: 3
        function: ldv_dispatch_insmod_register_10_3
      value: '! multithreaded || ((~ ((unsigned long )jiffies) & 0UL) == 0UL && ((unsigned
        long )jiffies & 0UL) == 0UL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7662
        column: 3
        function: ldv_dispatch_irq_register_8_3
      value: '! multithreaded || ((~ ((unsigned long )jiffies) & 0UL) == 0UL && ((unsigned
        long )jiffies & 0UL) == 0UL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7679
        column: 3
        function: ldv_dispatch_register_7_4
      value: '! multithreaded || ((~ ((unsigned long )jiffies) & 0UL) == 0UL && ((unsigned
        long )jiffies & 0UL) == 0UL)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7630
        column: 3
        function: ldv_dispatch_insmod_register_10_3
      value: '! multithreaded || ((irda_debug & 0U) == 0U && (~ irda_debug & 0U) ==
        0U)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7662
        column: 3
        function: ldv_dispatch_irq_register_8_3
      value: '! multithreaded || ((irda_debug & 0U) == 0U && (~ irda_debug & 0U) ==
        0U)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7679
        column: 3
        function: ldv_dispatch_register_7_4
      value: '! multithreaded || ((irda_debug & 0U) == 0U && (~ irda_debug & 0U) ==
        0U)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7630
        column: 3
        function: ldv_dispatch_insmod_register_10_3
      value: '! multithreaded || ((io_speed & 0U) == 0U && (~ io_speed & 0U) == 0U)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7662
        column: 3
        function: ldv_dispatch_irq_register_8_3
      value: '! multithreaded || ((io_speed & 0U) == 0U && (~ io_speed & 0U) == 0U)'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
        line: 7679
        column: 3
        function: ldv_dispatch_register_7_4
      value: '! multithreaded || ((io_speed & 0U) == 0U && (~ io_speed & 0U) == 0U)'
      format: c_expression
