#define TCOBASE(p)     ((p)->tco_res->start)
 /* SMI Control and Enable Register */
 #define SMI_EN(p)      ((p)->smi_res->start)
+#define TCO_EN         (1 << 13)
+#define GBL_SMI_EN     (1 << 0)
 
 #define TCO_RLD(p)     (TCOBASE(p) + 0x00) /* TCO Timer Reload/Curr. Value */
 #define TCOv1_TMR(p)   (TCOBASE(p) + 0x01) /* TCOv1 Timer Initial Value*/
 
        tmrval = seconds_to_ticks(p, t);
 
-       /* For TCO v1 the timer counts down twice before rebooting */
-       if (p->iTCO_version == 1)
+       /*
+        * If TCO SMIs are off, the timer counts down twice before rebooting.
+        * Otherwise, the BIOS generally reboots when the SMI triggers.
+        */
+       if (p->smi_res &&
+           (SMI_EN(p) & (TCO_EN | GBL_SMI_EN)) != (TCO_EN | GBL_SMI_EN))
                tmrval /= 2;
 
        /* from the specs: */
                 * Disables TCO logic generating an SMI#
                 */
                val32 = inl(SMI_EN(p));
-               val32 &= 0xffffdfff;    /* Turn off SMI clearing watchdog */
+               val32 &= ~TCO_EN;       /* Turn off SMI clearing watchdog */
                outl(val32, SMI_EN(p));
        }