diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+        * Handle special Float values correctly for counterexamples. (#697)
+        * Update examples to compile with copilot-theorem >= 3.0. (#692)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -14,7 +14,7 @@
   <https://copilot-language.github.io>.
 
 
-version                   : 4.7
+version                   : 4.7.1
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -51,6 +51,7 @@
                           , containers            >= 0.4 && < 0.9
                           , data-default          >= 0.7 && < 0.9
                           , directory             >= 1.3 && < 1.4
+                          , fp-ieee               >= 0.1 && < 0.2
                           , libBF                 >= 0.6.2 && < 0.7
                           , mtl                   >= 2.0 && < 2.4
                           , panic                 >= 0.4.0 && < 0.5
@@ -62,8 +63,8 @@
                           , xml                   >= 1.3 && < 1.4
                           , what4                 >= 1.3 && < 1.8
 
-                          , copilot-core          >= 4.7 && < 4.8
-                          , copilot-prettyprinter >= 4.7 && < 4.8
+                          , copilot-core          >= 4.7.1 && < 4.8
+                          , copilot-prettyprinter >= 4.7.1 && < 4.8
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/src/Copilot/Theorem/What4.hs b/src/Copilot/Theorem/What4.hs
--- a/src/Copilot/Theorem/What4.hs
+++ b/src/Copilot/Theorem/What4.hs
@@ -77,8 +77,9 @@
 import Data.Parameterized.Nonce
 import Data.Parameterized.Some
 import qualified Data.Parameterized.Vector as V
-import GHC.Float (castWord32ToFloat, castWord64ToDouble)
+import GHC.Float (castWord32ToFloat, castWord64ToDouble, double2Float)
 import LibBF (BigFloat, bfToDouble, pattern NearEven)
+import Numeric.Floating.IEEE.NaN (getPayload, isSignaling, setPayload, setPayloadSignaling)
 import qualified Panic as Panic
 
 import Copilot.Theorem.What4.Translate
@@ -707,7 +708,7 @@
   XFloat e ->
     Some . CopilotValue CT.Float <$>
       iFloatGroundEval WFP.SingleFloatRepr e
-                       (realToFrac . fst . bfToDouble NearEven)
+                       (nanSafeDoubleToFloat . fst . bfToDouble NearEven)
                        fromRational
                        (castWord32ToFloat . fromInteger . BV.asUnsigned)
   XDouble e ->
@@ -757,3 +758,17 @@
         WB.FloatIEEERepr          -> ieeeK <$> WG.groundEval ge e
         WB.FloatRealRepr          -> realK <$> WG.groundEval ge e
         WB.FloatUninterpretedRepr -> uninterpK <$> WG.groundEval ge e
+
+    -- Convert a Double to a Float. This function takes care to preserve
+    -- special floating-point values, such as negative zero, infinity, and NaN
+    -- values.
+    nanSafeDoubleToFloat :: Double -> Float
+    nanSafeDoubleToFloat x
+        -- double2Float does not preserve the payloads of NaN values, so we
+        -- include a special case for translating NaNs.
+        | isNaN x && isSignaling x = setPayloadSignaling payload
+        | isNaN x                  = setPayload payload
+        | otherwise                = double2Float x
+      where
+        payload :: Float
+        payload = double2Float $ getPayload x