diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG
index 9072a0a43..63ea6878b 100644
--- a/copilot-bluespec/CHANGELOG
+++ b/copilot-bluespec/CHANGELOG
@@ -1,3 +1,7 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+        * Fix translation of special Float values to Bluespec. (#697)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal
index 3ac0839cf..ffaadaca2 100644
--- a/copilot-bluespec/copilot-bluespec.cabal
+++ b/copilot-bluespec/copilot-bluespec.cabal
@@ -1,6 +1,6 @@
 cabal-version             : >= 1.10
 name                      : copilot-bluespec
-version                   : 4.7
+version                   : 4.7.1
 synopsis                  : A compiler for Copilot targeting FPGAs.
 description               :
   This package is a back-end from Copilot to FPGAs in Bluespec.
@@ -51,8 +51,8 @@ library
                           , ieee754           >= 0.8.0  && < 0.9
                           , pretty            >= 1.1.2  && < 1.2
 
-                          , copilot-core      >= 4.7 && < 4.8
-                          , language-bluespec >= 0.1 && < 0.2
+                          , copilot-core      >= 4.7.1 && < 4.8
+                          , language-bluespec >= 0.1   && < 0.2
 
   exposed-modules         : Copilot.Compile.Bluespec
 
diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
index 39ff1ad22..2b71b3957 100644
--- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
+++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
@@ -18,7 +18,7 @@ import Data.String (IsString (..))
 import qualified Language.Bluespec.Classic.AST as BS
 import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
 import Numeric.Floating.IEEE.NaN (isSignaling, setPayloadSignaling, setPayload, getPayload)
-import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64)
+import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64, float2Double)
 
 -- Internal imports: Copilot
 import Copilot.Core
@@ -535,7 +535,7 @@ constTy ty =
     Word16    -> constInt ty . toInteger
     Word32    -> constInt ty . toInteger
     Word64    -> constInt ty . toInteger
-    Float     -> constFP ty . realToFrac
+    Float     -> constFP ty . nanSafeFloat2Double
     Double    -> constFP ty
 
     -- Translating a Copilot array literal to a Bluespec Vector is somewhat
@@ -563,6 +563,20 @@ constTy ty =
                , constTy ty'' val
                ))
              (toValues v))
+  where
+    -- Convert a Float to a Double. This function takes care to preserve
+    -- special floating-point values, such as negative zero, infinity, and NaN
+    -- values.
+    nanSafeFloat2Double :: Float -> Double
+    nanSafeFloat2Double x
+        -- float2Double does not preserve the payloads of NaN values, so we
+        -- include special cases for translating NaNs.
+        | isNaN x && isSignaling x = setPayloadSignaling payload
+        | isNaN x                  = setPayload payload
+        | otherwise                = float2Double x
+      where
+        payload :: Double
+        payload = float2Double $ getPayload x
 
 -- | Transform a list of Copilot Core expressions of a given 'Type' into a
 -- Bluespec @Vector@ expression.
diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG
index 856d51497..74c6c1dd4 100644
--- a/copilot-c99/CHANGELOG
+++ b/copilot-c99/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
         * Raise error when compiling empty arrays or structs. (#695)
diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal
index 0567e9416..d9802bd42 100644
--- a/copilot-c99/copilot-c99.cabal
+++ b/copilot-c99/copilot-c99.cabal
@@ -1,6 +1,6 @@
 cabal-version             : >= 1.10
 name                      : copilot-c99
-version                   : 4.7
+version                   : 4.7.1
 synopsis                  : A compiler for Copilot targeting C99.
 description               :
   This package is a back-end from Copilot to C.
@@ -45,7 +45,7 @@ library
                           , mtl                 >= 2.2 && < 2.4
                           , pretty              >= 1.1 && < 1.2
 
-                          , copilot-core        >= 4.7   && < 4.8
+                          , copilot-core        >= 4.7.1 && < 4.8
                           , language-c99        >= 0.2.0 && < 0.3
                           , language-c99-simple >= 0.3   && < 0.4
 
diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG
index 671e39ef6..4a019a359 100644
--- a/copilot-core/CHANGELOG
+++ b/copilot-core/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal
index 6d99e77d6..ee463977c 100644
--- a/copilot-core/copilot-core.cabal
+++ b/copilot-core/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             4.7
+version:             4.7.1
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG
index c2920d179..53984488e 100644
--- a/copilot-interpreter/CHANGELOG
+++ b/copilot-interpreter/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal
index 9ef09f117..0303bf17b 100644
--- a/copilot-interpreter/copilot-interpreter.cabal
+++ b/copilot-interpreter/copilot-interpreter.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-interpreter
-version:             4.7
+version:             4.7.1
 synopsis:            Interpreter for Copilot.
 description:
   Interpreter for Copilot.
@@ -44,7 +44,7 @@ library
     base       >= 4.9 && < 5,
     pretty     >= 1.0 && < 1.2,
 
-    copilot-core >= 4.7 && < 4.8
+    copilot-core >= 4.7.1 && < 4.8
 
   exposed-modules:
 
diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG
index 4751f7061..069d20f5d 100644
--- a/copilot-language/CHANGELOG
+++ b/copilot-language/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal
index 740bb2b8c..2cfab8eb8 100644
--- a/copilot-language/copilot-language.cabal
+++ b/copilot-language/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             4.7
+version:             4.7.1
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -42,9 +42,9 @@ library
                , data-reify            >= 0.6  && < 0.7
                , mtl                   >= 2.0  && < 3
 
-               , copilot-core          >= 4.7 && < 4.8
-               , copilot-interpreter   >= 4.7 && < 4.8
-               , copilot-theorem       >= 4.7 && < 4.8
+               , copilot-core          >= 4.7.1 && < 4.8
+               , copilot-interpreter   >= 4.7.1 && < 4.8
+               , copilot-theorem       >= 4.7.1 && < 4.8
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG
index 171b9b7d7..19b510a63 100644
--- a/copilot-libraries/CHANGELOG
+++ b/copilot-libraries/CHANGELOG
@@ -1,3 +1,8 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+        * Add stream analysis module. (#726)
+        * Add state machine module. (#728)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal
index e194daf78..85b117f63 100644
--- a/copilot-libraries/copilot-libraries.cabal
+++ b/copilot-libraries/copilot-libraries.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-libraries
-version:             4.7
+version:             4.7.1
 synopsis:            Libraries for the Copilot language.
 description:
   Libraries for the Copilot language.
@@ -41,13 +41,15 @@ library
                , containers       >= 0.4 && < 0.9
                , mtl              >= 2.0 && < 2.4
                , parsec           >= 2.0 && < 3.2
-               , copilot-language >= 4.7 && < 4.8
+               , copilot-language >= 4.7.1 && < 4.8
 
   exposed-modules:
-      Copilot.Library.Libraries
+      Copilot.Library.Analysis
+    , Copilot.Library.Libraries
     , Copilot.Library.Clocks
     , Copilot.Library.LTL
     , Copilot.Library.PTLTL
+    , Copilot.Library.StateMachines
     , Copilot.Library.Statistics
     , Copilot.Library.RegExp
     , Copilot.Library.Utils
diff --git a/copilot-libraries/src/Copilot/Library/Analysis.hs b/copilot-libraries/src/Copilot/Library/Analysis.hs
new file mode 100644
index 000000000..240addd7c
--- /dev/null
+++ b/copilot-libraries/src/Copilot/Library/Analysis.hs
@@ -0,0 +1,23 @@
+-- | Formally analyze streams.
+module Copilot.Library.Analysis
+    ( triviallyTrue
+    , triviallyFalse
+    )
+  where
+
+-- External imports.
+import Prelude hiding (not)
+
+-- Internal imports.
+import Copilot.Language      (Stream, forAll, not)
+import Copilot.Language.Spec (Prop, Universal)
+
+-- | Property that captures whether a stream is trivially true, meaning that
+-- there is no way to make it false.
+triviallyTrue :: Stream Bool -> Prop Universal
+triviallyTrue = forAll
+
+-- | Property that captures whether a stream is trivially false, meaning that
+-- there is no way to make it true.
+triviallyFalse :: Stream Bool -> Prop Universal
+triviallyFalse = triviallyTrue . not
diff --git a/copilot-libraries/src/Copilot/Library/StateMachines.hs b/copilot-libraries/src/Copilot/Library/StateMachines.hs
new file mode 100644
index 000000000..37121b1a0
--- /dev/null
+++ b/copilot-libraries/src/Copilot/Library/StateMachines.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | Simulate state machines using streams.
+module Copilot.Library.StateMachines where
+
+import Copilot.Language (Stream, Typed, constant, ifThenElse, (&&), (++), (==))
+import Prelude          hiding ((&&), (++), (==))
+
+-- | A definition of a state machine where some elements are defined
+-- as streams.
+--
+-- A state machine is defined by an initial state, a final state, a no
+-- transition stream (true when tere is no input coming in), a list of
+-- transitions, and a bad state.
+type StateMachine a = (a, a, Stream Bool, [(a, Stream Bool, a)], a)
+
+-- | Produce a stream that, at any given time, contains the current state of
+-- the state machine.
+stateMachine :: forall a . (Eq a, Typed a) => StateMachine a -> Stream a
+stateMachine (initial, final, noInputData, transitions, bad) = state
+  where
+    state         = ifThenElses transitions
+    previousState = [initial] ++ state
+
+    ifThenElses :: [(a, Stream Bool, a)] -> Stream a
+    ifThenElses [] =
+      ifThenElse (previousState == constant final && noInputData)
+        (constant final)
+        (constant bad)
+
+    ifThenElses ((s1, i, s2):ss) =
+      ifThenElse
+        (previousState == constant s1 && i)
+        (constant s2)
+        (ifThenElses ss)
+
+-- | Produce a stream that, at any given time, contains the current state of
+-- the state machine as the numeric representation of an enum.
+stateMachineEnum :: (Eq b, Typed b, Num b, Enum a)
+                 => StateMachine a
+                 -> Stream b
+stateMachineEnum (initial, final, noInputData, transitions, bad) =
+    stateMachine (fe initial, fe final, noInputData, transitionsE, fe bad)
+  where
+    transitionsE = map (\(s1, t, s2) -> (fe s1, t, fe s2)) transitions
+    fe           = fromIntegral . fromEnum
diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG
index efa6ccf51..a8e6d3e12 100644
--- a/copilot-prettyprinter/CHANGELOG
+++ b/copilot-prettyprinter/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal
index f6f5fcc57..c40511c43 100644
--- a/copilot-prettyprinter/copilot-prettyprinter.cabal
+++ b/copilot-prettyprinter/copilot-prettyprinter.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-prettyprinter
-version:             4.7
+version:             4.7.1
 synopsis:            A prettyprinter of Copilot Specifications.
 description:
   A prettyprinter of Copilot specifications.
@@ -45,7 +45,7 @@ library
     base   >= 4.9 && < 5,
     pretty >= 1.0 && < 1.2,
 
-    copilot-core >= 4.7 && < 4.8
+    copilot-core >= 4.7.1 && < 4.8
 
   exposed-modules:
 
diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
index 4aaf2cf97..03facaf36 100644
--- a/copilot-theorem/CHANGELOG
+++ b/copilot-theorem/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/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal
index f8b4ff57e..cd9d2e00e 100644
--- a/copilot-theorem/copilot-theorem.cabal
+++ b/copilot-theorem/copilot-theorem.cabal
@@ -14,7 +14,7 @@ description:
   <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 @@ library
                           , 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 @@ library
                           , 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/copilot-theorem/examples/BoyerMoore.hs b/copilot-theorem/examples/BoyerMoore.hs
index d4cebf638..47fe790af 100644
--- a/copilot-theorem/examples/BoyerMoore.hs
+++ b/copilot-theorem/examples/BoyerMoore.hs
@@ -5,7 +5,7 @@ module BoyerMoore where
 
 import Copilot.Language hiding (length)
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (debug, def, induction, z3)
 
 import Copilot.Core.Type
 
@@ -71,7 +71,7 @@ spec = do
     maj = majorityVote ss
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = False }
+induct = induction def { debug = False } z3
 
 -- | Initial value for a given type.
 --
diff --git a/copilot-theorem/examples/Grey.hs b/copilot-theorem/examples/Grey.hs
index 9a1ca4319..91500ba1a 100644
--- a/copilot-theorem/examples/Grey.hs
+++ b/copilot-theorem/examples/Grey.hs
@@ -4,7 +4,7 @@ module Grey where
 
 import Copilot.Language
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (Options (..), def, induction, kInduction, z3)
 
 import Prelude ()
 import Data.String (fromString)
@@ -32,7 +32,7 @@ spec = do
     r  = extern "reset" Nothing
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = False }
+induct = induction def { debug = False } z3
 
 kinduct :: Word32 -> Proof Universal
-kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False }
+kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3
diff --git a/copilot-theorem/examples/Incr.hs b/copilot-theorem/examples/Incr.hs
index 3c39a008d..dd6ccdc42 100644
--- a/copilot-theorem/examples/Incr.hs
+++ b/copilot-theorem/examples/Incr.hs
@@ -4,7 +4,7 @@ import Prelude ()
 import Copilot.Language
 
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (debug, def, induction, z3)
 
 spec = do
   bounds <- prop "bounds" (forAll $ x < 255)
@@ -16,4 +16,4 @@ spec = do
     x = [2] ++ (1 + x)
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = True }
+induct = induction def { debug = True } z3
diff --git a/copilot-theorem/examples/SerialBoyerMoore.hs b/copilot-theorem/examples/SerialBoyerMoore.hs
index 5f0d42092..eb858a6a6 100644
--- a/copilot-theorem/examples/SerialBoyerMoore.hs
+++ b/copilot-theorem/examples/SerialBoyerMoore.hs
@@ -4,7 +4,7 @@ module SerialBoyerMoore where
 
 import Copilot.Language
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (Options (..), def, induction, kInduction, z3)
 
 import Prelude ()
 import Data.String (fromString)
@@ -56,7 +56,7 @@ spec = do
     (p, s, j) = majority input
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = False }
+induct = induction def { debug = False } z3
 
 kinduct :: Word32 -> Proof Universal
-kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False }
+kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3
diff --git a/copilot-theorem/examples/SphericalWCV.hs b/copilot-theorem/examples/SphericalWCV.hs
index 74b899583..06d203adf 100644
--- a/copilot-theorem/examples/SphericalWCV.hs
+++ b/copilot-theorem/examples/SphericalWCV.hs
@@ -8,7 +8,7 @@ import Prelude ()
 import Copilot.Language
 import Copilot.Language.Reify
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (debug, def, onlySat, onlyValidity, z3)
 
 import qualified Copilot.Language.Operators.Propositional as P
 
@@ -241,7 +241,7 @@ localConvexity = do
   theorem "6"  (P.not (forAll $ locallyConvex tau)) arithSat
 
 arith :: Proof Universal
-arith    = onlyValidity def { nraNLSat = True, debug = False }
+arith    = onlyValidity def { debug = False } z3
 
 arithSat :: Proof Existential
-arithSat = onlySat      def { nraNLSat = True, debug = False }
+arithSat = onlySat      def { debug = False } z3
diff --git a/copilot-theorem/examples/WCV.hs b/copilot-theorem/examples/WCV.hs
index 62c27f287..c0f267c68 100644
--- a/copilot-theorem/examples/WCV.hs
+++ b/copilot-theorem/examples/WCV.hs
@@ -5,7 +5,7 @@ import Prelude ()
 import Copilot.Language
 import Copilot.Language.Reify
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (debug, def, onlySat, onlyValidity, z3)
 
 import qualified Copilot.Language.Operators.Propositional as P
 
@@ -165,7 +165,7 @@ localConvexity = do
   theorem "6"  (P.not (forAll $ locallyConvex tau)) arithSat
 
 arith :: Proof Universal
-arith    = onlyValidity def { nraNLSat = True, debug = False }
+arith    = onlyValidity def { debug = False } z3
 
 arithSat :: Proof Existential
-arithSat = onlySat      def { nraNLSat = True, debug = False }
+arithSat = onlySat      def { debug = False } z3
diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 51ed6e8ff..97e55a852 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -77,8 +77,9 @@ import Data.Parameterized.NatRepr
 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 @@ valFromExpr ge xe = case xe of
   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 @@ valFromExpr ge xe = case xe of
         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
diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG
index 049ec2243..a2b4dd530 100644
--- a/copilot-verifier/CHANGELOG
+++ b/copilot-verifier/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
         * Relax version constraints on what4. (#716)
diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
index c7bf36a10..339892ec9 100644
--- a/copilot-verifier/copilot-verifier.cabal
+++ b/copilot-verifier/copilot-verifier.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          copilot-verifier
-Version:       4.7
+Version:       4.7.1
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com
 Copyright:     (c) Galois, Inc 2021-2024
@@ -45,9 +45,9 @@ common bldflags
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot-c99 >= 4.7 && < 4.8,
-    copilot-core >= 4.7 && < 4.8,
-    copilot-theorem >= 4.7 && < 4.8,
+    copilot-c99 >= 4.7.1 && < 4.8,
+    copilot-core >= 4.7.1 && < 4.8,
+    copilot-theorem >= 4.7.1 && < 4.8,
     crucible >= 0.7.1 && < 0.8,
     crucible-llvm >= 0.7 && < 0.8,
     crux >= 0.7.1 && < 0.8,
@@ -80,10 +80,10 @@ library copilot-verifier-examples
   hs-source-dirs: examples
   build-depends:
     case-insensitive,
-    copilot >= 4.7 && < 4.8,
-    copilot-language >= 4.7 && < 4.8,
-    copilot-libraries >= 4.7 && < 4.8,
-    copilot-prettyprinter >= 4.7 && < 4.8,
+    copilot >= 4.7.1 && < 4.8,
+    copilot-language >= 4.7.1 && < 4.8,
+    copilot-libraries >= 4.7.1 && < 4.8,
+    copilot-prettyprinter >= 4.7.1 && < 4.8,
     copilot-verifier
   exposed-modules:
     Copilot.Verifier.Examples
diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG
index 402ec34d5..0735d51ab 100644
--- a/copilot-visualizer/CHANGELOG
+++ b/copilot-visualizer/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
         * Relax version constraints on ogma-extra. (#716)
diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal
index 0500c1b43..5e8735ea4 100644
--- a/copilot-visualizer/copilot-visualizer.cabal
+++ b/copilot-visualizer/copilot-visualizer.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >= 1.10
 name:                copilot-visualizer
-version:             4.7
+version:             4.7.1
 synopsis:            Visualizer for Copilot.
 description:
   Visualizer for Copilot.
@@ -65,10 +65,10 @@ library
     text       >= 1.2.3.1 && < 2.2,
     websockets >= 0.12.7  && < 0.14,
 
-    copilot             >= 4.7 && < 4.8,
-    copilot-core        >= 4.7 && < 4.8,
-    copilot-interpreter >= 4.7 && < 4.8,
-    copilot-language    >= 4.7 && < 4.8
+    copilot             >= 4.7.1 && < 4.8,
+    copilot-core        >= 4.7.1 && < 4.8,
+    copilot-interpreter >= 4.7.1 && < 4.8,
+    copilot-language    >= 4.7.1 && < 4.8
 
   exposed-modules:
 
diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG
index dd34bc70f..f58dd30e6 100644
--- a/copilot/CHANGELOG
+++ b/copilot/CHANGELOG
@@ -1,3 +1,6 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal
index 68ff811ec..ace61023d 100644
--- a/copilot/copilot.cabal
+++ b/copilot/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             4.7
+version:             4.7.1
 cabal-version:       >= 1.10
 license:             BSD3
 license-file:        LICENSE
@@ -52,12 +52,12 @@ library
                      , directory             >= 1.3  && < 1.4
                      , filepath              >= 1.4  && < 1.6
 
-                     , copilot-core          >= 4.7 && < 4.8
-                     , copilot-theorem       >= 4.7 && < 4.8
-                     , copilot-language      >= 4.7 && < 4.8
-                     , copilot-libraries     >= 4.7 && < 4.8
-                     , copilot-c99           >= 4.7 && < 4.8
-                     , copilot-prettyprinter >= 4.7 && < 4.8
+                     , copilot-core          >= 4.7.1 && < 4.8
+                     , copilot-theorem       >= 4.7.1 && < 4.8
+                     , copilot-language      >= 4.7.1 && < 4.8
+                     , copilot-libraries     >= 4.7.1 && < 4.8
+                     , copilot-c99           >= 4.7.1 && < 4.8
+                     , copilot-prettyprinter >= 4.7.1 && < 4.8
 
 
     exposed-modules: Language.Copilot, Language.Copilot.Main