diff -r 235ff1c046df src/dev/arm/gic_pl390.cc
--- a/src/dev/arm/gic_pl390.cc	Fri Apr 03 11:42:11 2015 -0500
+++ b/src/dev/arm/gic_pl390.cc	Thu Apr 09 10:45:54 2015 +0100
@@ -525,7 +525,8 @@
         } else {
             uint32_t int_num = 1 << intNumToBit(iar.ack_id);
             if (!(activeInt[intNumToWord(iar.ack_id)] & int_num))
-                panic("Done handling interrupt that isn't active?\n");
+                warn("Done handling interrupt that isn't active: %d\n",
+                      intNumToBit(iar.ack_id));
             activeInt[intNumToWord(iar.ack_id)] &= ~int_num;
         }
         updateRunPri();