diff --git a/acl2.lisp b/acl2.lisp
index 036657d902..c2b7e4fad9 100644
--- a/acl2.lisp
+++ b/acl2.lisp
@@ -1963,11 +1963,7 @@ ACL2 from scratch.")
                (* *my-most-positive-double-float*
                   *my-most-positive-double-float*)
                (error () 0.0d0))
-              'double-float))
-     #+sbcl
-     (member :overflow
-             (cadr (member :traps
-                           (sb-int:get-floating-point-modes)))))
+              'double-float)))
   (error "This Lisp is unsuitable for ACL2, because it failed ~%a check that ~
           floating-point overflow causes an error."))
 
diff --git a/float-raw.lisp b/float-raw.lisp
index 1364491fdf..e6d0417971 100644
--- a/float-raw.lisp
+++ b/float-raw.lisp
@@ -46,13 +46,13 @@
 ; #.*infinity-double* and #.*negative-infinity-double*), so we do so, but we
 ; don't bother testing for Nan in LispWorks.
 
-; We return form unchanged in other than Allegro CL and LispWorks, because we
+; We return form unchanged in other than Allegro CL, LispWorks, and SBCL, because we
 ; already know that an error is signalled on overflow for other Lisps that host
 ; ACL2; see break-on-overflow-and-nan.
 
-  #-(or allegro lispworks)
+  #-(or allegro lispworks sbcl)
   (declare (ignore op))
-  #-(or allegro lispworks)
+  #-(or allegro lispworks sbcl)
   form
   #+allegro
   `(let ((result ,form))
@@ -65,6 +65,14 @@
      (when (or (= result +1D++0) (= result -1D++0))
        (error "Floating-point overflow for a call of ~s"
               ',op))
+     result)
+  #+sbcl
+  `(let ((result ,form))
+     (when (or (sb-ext:float-nan-p result)
+               (= result sb-ext:double-float-positive-infinity)
+               (= result sb-ext:double-float-negative-infinity))
+       (error "Floating-point exception for a call of ~s"
+              ',op))
      result))
 
 (defmacro defun-df-binary (name op)