diff --git a/libsel4vm/src/arch/arm/vgic/gicv2.h b/libsel4vm/src/arch/arm/vgic/gicv2.h
index 39dc45443..8ac96a817 100644
--- a/libsel4vm/src/arch/arm/vgic/gicv2.h
+++ b/libsel4vm/src/arch/arm/vgic/gicv2.h
@@ -97,6 +97,11 @@ struct gic_dist_map {
     uint32_t component_id[4];                           /* [0xFF0, 0xFFF] */
 };
 
+static inline bool gic_dist_is_enabled(vgic_t *vgic)
+{
+    return (0 != vgic->dist->enable);
+}
+
 static inline void vgic_dist_set_ctlr(vgic_t *vgic, uint32_t data)
 {
     /* ToDo: we should care about bit 0 only and ignore all the others. */
diff --git a/libsel4vm/src/arch/arm/vgic/vdist.h b/libsel4vm/src/arch/arm/vgic/vdist.h
index 5e3e3af0b..c541e81ef 100644
--- a/libsel4vm/src/arch/arm/vgic/vdist.h
+++ b/libsel4vm/src/arch/arm/vgic/vdist.h
@@ -189,7 +189,7 @@ static int vgic_dist_set_pending_irq(vgic_t *vgic, vm_vcpu_t *vcpu, int irq)
 
     struct virq_handle *virq_data = virq_find_irq_data(vgic, vcpu, irq);
 
-    if (!virq_data || !vgic->dist->enable || !is_enabled(vgic->dist, irq, vcpu->vcpu_id)) {
+    if (!virq_data || !gic_dist_is_enabled(vgic) || !is_enabled(vgic->dist, irq, vcpu->vcpu_id)) {
         DDIST("IRQ not enabled (%d) on vcpu %d\n", irq, vcpu->vcpu_id);
         return -1;
     }