kvm_debug("Set active, clear distributor: 0x%x\n", vlr.state);
                vgic_irq_clear_active(vcpu, irq);
                vgic_update_state(vcpu->kvm);
-       } else if (vgic_dist_irq_is_pending(vcpu, irq)) {
+       } else {
+               WARN_ON(!vgic_dist_irq_is_pending(vcpu, irq));
                vlr.state |= LR_STATE_PENDING;
                kvm_debug("Set pending: 0x%x\n", vlr.state);
        }
        } else {
                if (level_triggered) {
                        vgic_dist_irq_clear_level(vcpu, irq_num);
-                       if (!vgic_dist_irq_soft_pend(vcpu, irq_num))
+                       if (!vgic_dist_irq_soft_pend(vcpu, irq_num)) {
                                vgic_dist_irq_clear_pending(vcpu, irq_num);
+                               vgic_cpu_irq_clear(vcpu, irq_num);
+                               if (!compute_pending_for_cpu(vcpu))
+                                       clear_bit(cpuid, dist->irq_pending_on_cpu);
+                       }
                }
 
                ret = false;