diff --git a/pkgs/by-name/ac/acl2/0002-sbcl-fp-trap-fallback.patch b/pkgs/by-name/ac/acl2/0002-sbcl-fp-trap-fallback.patch
new file mode 100644
index 000000000000..3d3a894edbd5
--- /dev/null
+++ b/pkgs/by-name/ac/acl2/0002-sbcl-fp-trap-fallback.patch
@@ -0,0 +1,53 @@
+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)
diff --git a/pkgs/by-name/ac/acl2/package.nix b/pkgs/by-name/ac/acl2/package.nix
index 78929aaf06ae..df06ba483a57 100644
--- a/pkgs/by-name/ac/acl2/package.nix
+++ b/pkgs/by-name/ac/acl2/package.nix
@@ -62,6 +62,13 @@ stdenv.mkDerivation rec {
       libssl = "${lib.getLib openssl}/lib/libssl${stdenv.hostPlatform.extensions.sharedLibrary}";
       libcrypto = "${lib.getLib openssl}/lib/libcrypto${stdenv.hostPlatform.extensions.sharedLibrary}";
     })
+  ]
+  ++ lib.optionals (stdenv.hostPlatform.system == "aarch64-linux") [
+    # ACL2 8.6 assumes SBCL can enable floating-point traps. On
+    # aarch64-linux, SBCL can leave :TRAPS NIL after enabling them, so use
+    # ACL2's existing exceptional-float checking path instead. See:
+    # https://github.com/acl2-devel/acl2-devel/commit/0632b37adffb6b5fd71d8438d519133281f837ec
+    ./0002-sbcl-fp-trap-fallback.patch
   ];
 
   # We need the timestamps on the source tree to be stable for certification to