diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,32 @@
 * Hackage: <http://hackage.haskell.org/package/sbv>
 * GitHub:  <http://github.com/LeventErkok/sbv>
 
+### Version 14.3, 2026-06-19
+
+  * Improve fpRoundToIntegralH to remove redundant internal check. Thanks to Ryan Scott for the report.
+
+  * Add support for arctan/arcsin/arccos in CVC5. Thanks to Ryan Scott for pointing out support for it.
+
+  * Improved backed-solver communication so that if a solver returns an error message SBV now makes
+    sure it gets captured and displayed properly before the solver-process itselfs terminates.
+
+  * Drop support for pi as an SReal: The whole premise of SReal is it represents algebraic-reals
+    (i.e., those that are roots of polynomials) exactly. But pi is not representable as such, since
+    it's transcendental. Older versions of SBV used an approximation, but that's confusing to say
+    the least, and downright wrong. Note that you can still use pi at floating-point types, where
+    precision loss is built into the semantics.
+
+  * Fix the enumeration quasi-quoter for a zero step: `[sEnum| 1, 1 .. 5 |]` is now the
+    (semantically infinite) list of 1's, instead of the empty list.
+
+  * Soundness fix for termination measures: a real-valued measure is now rejected at compile
+    time. The reals are not well-ordered (an infinite descending chain like 1, 1/2, 1/4, ...
+    never reaches a minimum), so a non-negative, strictly-decreasing real measure does not
+    imply termination. Use an integer-valued measure instead.
+
+  * Termination measures may now be given over the bounded bit-vector types (`Word8`..`Word64`,
+    `Int8`..`Int64`, `WordN n`, `IntN n`), in addition to the integer/float types supported before.
+
 ### Version 14.2, 2026-06-05
 
   * Fix float to integer conversions, which were ignoring the rounding mode previously. Thanks to
diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs
--- a/Data/SBV/Core/Model.hs
+++ b/Data/SBV/Core/Model.hs
@@ -1230,6 +1230,20 @@
 instance Zero Integer where
    zero = literal 0
 
+-- | Bounded bit-vectors as measures. These are all sound: each is a finite type, so a
+-- non-negative, strictly-decreasing chain of values is necessarily finite. (The default
+-- @nonNeg x = x .>= 0@ works for both the unsigned and signed cases.)
+instance Zero Word8  where zero = literal 0
+instance Zero Word16 where zero = literal 0
+instance Zero Word32 where zero = literal 0
+instance Zero Word64 where zero = literal 0
+instance Zero Int8   where zero = literal 0
+instance Zero Int16  where zero = literal 0
+instance Zero Int32  where zero = literal 0
+instance Zero Int64  where zero = literal 0
+instance (KnownNat n, BVIsNonZero n) => Zero (WordN n) where zero = literal 0
+instance (KnownNat n, BVIsNonZero n) => Zero (IntN  n) where zero = literal 0
+
 -- NB. We would like to use 'Data.SBV.Tuple.untuple' in the 'nonNeg' definitions below,
 -- but 'Data.SBV.Tuple' imports 'Data.SBV.Core.Model', creating a circular dependency.
 -- So we extract components at the SVal level using 'TupleAccess' directly.
@@ -1262,9 +1276,19 @@
 instance Zero Double where
    zero = literal 0
 
--- | An algebraic real as a measure
-instance Zero AlgReal where
-   zero = literal 0
+-- | Algebraic reals are /not/ permitted as measures, and we reject them at compile time.
+-- The reals are dense, hence not well-ordered: a merely non-negative and strictly-decreasing
+-- real measure does not imply termination (e.g. the chain @1, 1\/2, 1\/4, ...@ descends forever
+-- without reaching a minimum). Use an integer-valued measure instead.
+instance TypeError (     'Text "A termination measure may not have a real-valued result."
+                   ':$$: 'Text ""
+                   ':$$: 'Text "The reals are not well-ordered: an infinite descending chain such as"
+                   ':$$: 'Text "1, 1/2, 1/4, ... has no least element, so a non-negative and strictly"
+                   ':$$: 'Text "decreasing real measure does not imply termination."
+                   ':$$: 'Text ""
+                   ':$$: 'Text "Use an integer-valued measure instead (e.g. a count of remaining steps)."
+                   ) => Zero AlgReal where
+   zero = error "Data.SBV.Zero(AlgReal): unreachable"
 
 -- | A floating-point as a measure
 instance ValidFloat eb sb => Zero (FloatingPoint eb sb) where
@@ -2882,7 +2906,23 @@
 -- we do not constant fold these values (except for pi), as Haskell doesn't really have any means of computing
 -- them for arbitrary rationals.
 instance {-# OVERLAPPING #-} Floating SReal where
-  pi      = fromRational . toRational $ (pi :: Double)  -- Perhaps not good enough?
+  -- Should we support pi? It's a transcendental value, and our SReal type has no way of representing
+  -- this quantity with the required fidelity. (SReal can only support roots of polynomials and rationals
+  -- correctly, not transcendentals.) One option is to use an approximation here. But that goes against the
+  -- whole idea of Real being infinitely precise. Another option is to see if the solver has support for it, such
+  -- as CVC5, which has the constant real.pi. Alas, that has its problems: In models CVC5 uses real.pi as a
+  -- model value, which we have no way of properly supporting back as a Haskell value. Worse: It uses it in
+  -- expressions like 1 + real.pi, which we don't have an evaluator for. So, we simply say not supported.
+  -- If you want it for reals, you'll have to plugin your own "approximation" for it, and thus be aware of the
+  -- limitations of that choice.
+  pi      = error $ unlines [ ""
+                            , "*** Data.SBV.SReal: Cannot represent pi as an SReal value."
+                            , "***"
+                            , "*** Usual trick is to use an approximation if that suits your purpose,"
+                            , "*** or use solver-specific constants when applicable. Please get in touch"
+                            , "*** if you'd like to explore ideas here."
+                            ]
+
   exp     = lift1SReal NR_Exp
   log     = lift1SReal NR_Log
   sqrt    = lift1SReal NR_Sqrt
diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs
--- a/Data/SBV/Core/Symbolic.hs
+++ b/Data/SBV/Core/Symbolic.hs
@@ -57,7 +57,7 @@
   , MonadQuery(..), QueryT(..), Query, QueryState(..), QueryContext(..)
   , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), TPOptions(..), SMTEngine
   , validationRequested, outputSVal, ProgInfo(..), mustIgnoreVar, getRootState
-  , LambdaInfo(..)
+  , LambdaInfo(..), showNROp
   ) where
 
 import Control.DeepSeq             (NFData(..))
@@ -321,7 +321,8 @@
    show FP_IsNegative        = "fp.isNegative"
    show FP_IsPositive        = "fp.isPositive"
 
--- | Non-linear operations
+-- | Non-linear operations. We do *not* on purpose deriving Show here, nor give a show instance,
+-- since different solvers call these functions with different names.
 data NROp = NR_Sin
           | NR_Cos
           | NR_Tan
@@ -337,22 +338,31 @@
           | NR_Pow
           deriving (Eq, Ord, G.Data, NFData, Generic)
 
--- | The show instance carefully arranges for these to be printed as it can be understood by dreal
-instance Show NROp where
-  show NR_Sin  = "sin"
-  show NR_Cos  = "cos"
-  show NR_Tan  = "tan"
-  show NR_ASin = "asin"
-  show NR_ACos = "acos"
-  show NR_ATan = "atan"
-  show NR_Sinh = "sinh"
-  show NR_Cosh = "cosh"
-  show NR_Tanh = "tanh"
-  show NR_Sqrt = "sqrt"
-  show NR_Exp  = "exp"
-  show NR_Log  = "log"
-  show NR_Pow  = "pow"
+-- | Show a non-linear op. Unfortunately this can't be generically done since different
+-- solvers use different names for some of these ops.
+showNROp :: Solver -> NROp -> String
+showNROp slvr = sh
+  where sh NR_Sin  = "sin"
+        sh NR_Cos  = "cos"
+        sh NR_Tan  = "tan"
+        sh NR_ASin = arc ++ "sin"
+        sh NR_ACos = arc ++ "cos"
+        sh NR_ATan = arc ++ "tan"
+        sh NR_Sinh = "sinh"
+        sh NR_Cosh = "cosh"
+        sh NR_Tanh = "tanh"
+        sh NR_Sqrt = "sqrt"
+        sh NR_Exp  = "exp"
+        sh NR_Log  = "log"
+        sh NR_Pow  = "pow"
 
+        -- DReal uses asin/acos etc. CVC5 uses arcsin. Other solvers probably
+        -- don't even support these. But this isn't the right place to bail-out
+        -- about it; so we just put "arc" following CVC5 here.
+        arc = case slvr of
+                DReal -> "a"
+                _     -> "arc"
+
 -- | Pseudo-boolean operations
 data PBOp = PB_AtMost  Int        -- ^ At most k
           | PB_AtLeast Int        -- ^ At least k
@@ -583,7 +593,7 @@
 
   show (IEEEFP w)           = show w
 
-  show (NonLinear w)        = show w
+  show (NonLinear w)        = showNROp DReal w -- Just use DReal here, only used for debugging
 
   show (PseudoBoolean p)    = show p
 
diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs
--- a/Data/SBV/List.hs
+++ b/Data/SBV/List.hs
@@ -1200,6 +1200,16 @@
    -- | @`enumFromThenTo` m n@. Symbolic version of @[m, m' .. n]@
    enumFromThenTo :: SymVal a => SBV a -> SBV a -> SBV a -> SList a
 
+   -- | @`enumFromThenTo`@ with an optionally statically-known integer step. The sEnum quasiquoter
+   -- supplies @`Just` d@ for @[m, m' .. n]@ when @m'@ is @m@ shifted by a compile-time integer
+   -- constant (e.g. @[m, m-1 .. n]@ gives @-1@); otherwise it supplies `Nothing`. Instances with
+   -- exact arithmetic (integers, reals) use the hint to constant-fold the step, so the @step == 0@
+   -- infinite-list branch (and its productive helper) drops out; every other instance ignores the
+   -- hint and falls back to 'enumFromThenTo', preserving its exact semantics. Not meant to be called
+   -- directly; the default is correct for any instance.
+   enumFromThenToH :: SymVal a => SBV a -> SBV a -> SBV a -> Maybe Integer -> SList a
+   enumFromThenToH from thn to _ = enumFromThenTo from thn to
+
 -- | 'EnumSymbolic' instance for words
 instance {-# OVERLAPPABLE #-} (SymVal a, Bounded a, Integral a, Num a, Num (SBV a)) => EnumSymbolic a where
   succ = smtFunction "EnumSymbolic.succ" (\x -> ite (x .== maxBound) (some "EnumSymbolic.succ.maxBound" (const sTrue)) (x+1))
@@ -1232,23 +1242,34 @@
    toEnum   = id
    fromEnum = id
 
-   enumFrom   n = enumFromThen   n (n+1)
-   enumFromTo n = enumFromThenTo n (n+1)
+   enumFrom   n   = enumFromThen          n (n+1)
+   enumFromTo n m = enumFromThenToInteger n m 1
 
    enumFromThen x y = go x (y-x)
      where go = smtProductiveFunction "EnumSymbolic.Integer.enumFromThen" $ \start delta -> start .: go (start+delta) delta
 
-   enumFromThenTo x y z = ite (delta .>= 0) (up x delta z) (down x delta z)
-     where delta = y - x
+   enumFromThenTo x y z = enumFromThenToInteger x z (y - x)
 
-           up, down :: SInteger -> SInteger -> SInteger -> SList Integer
-           up    = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.up"
-                                          (\start _d end -> 0 `smax` (end - start + 1), [])
-                 $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up   (start + d) d end)
-           down  = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.down"
-                                          (\start _d end -> 0 `smax` (start - end + 1), [])
-                 $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end)
+   enumFromThenToH x y z mStep = enumFromThenToInteger x z (maybe (y - x) fromIntegral mStep)
 
+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
+-- if x <= z, and the empty list otherwise. We mirror that here.
+enumFromThenToInteger :: SInteger -> SInteger -> SInteger -> SList Integer
+enumFromThenToInteger x z delta = ite (delta .== 0)
+                                      (ite (x .<= z) (enumFromThen x x) [])
+                                $ ite (delta .>  0) (up x delta z) (down x delta z)
+  where -- The d==0 case is handled: 'up'/'down' are only *called* with d>0/d<0 (the d==0 case
+        -- is routed to the infinite-list branch above), and the guard's @d .<= 0@/@d .>= 0@ test
+        -- puts @d>0@/@d<0@ into the reaching condition, so measure verification never sees d==0.
+        -- (The integer measure does not divide by d, so there's no zero-denominator to worry about.)
+        up, down :: SInteger -> SInteger -> SInteger -> SList Integer
+        up    = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.up"
+                                       (\start _d end -> 0 `smax` (end - start + 1), [])
+              $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up   (start + d) d end)
+        down  = smtFunctionWithMeasure "EnumSymbolic.Integer.enumFromThenTo.down"
+                                       (\start _d end -> 0 `smax` (start - end + 1), [])
+              $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end)
+
 -- | 'EnumSymbolic instance for 'Float'. Note that the termination requirement as defined by the Haskell standard for floats state:
 --      > For Float and Double, the semantics of the enumFrom family is given by the rules for Int above,
 --      > except that the list terminates when the elements become greater than @e3 + i/2@ for positive increment @i@,
@@ -1260,23 +1281,39 @@
    toEnum   = sFromIntegral
    fromEnum = fromSFloat sRTZ
 
-   enumFrom   n = enumFromThen   n (n+1)
-   enumFromTo n = enumFromThenTo n (n+1)
+   enumFrom   n   = enumFromThen        n (n+1)
+   enumFromTo n m = enumFromThenToFloat n m 1
 
    enumFromThen x y = go 0 x (y-x)
      where go = smtProductiveFunction "EnumSymbolic.Float.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d
 
-   enumFromThenTo x y zIn = ite (delta .>= 0) (up 0 x delta z) (down 0 x delta z)
-     where delta, z :: SFloat
-           delta = y - x
-           z     = zIn + delta / 2
+   enumFromThenTo x y zIn = enumFromThenToFloat x zIn (y - x)
 
-           up, down :: SFloat -> SFloat -> SFloat -> SFloat -> SList Float
-           up   = smtFunctionWithMeasure "EnumSymbolic.Float.enumFromThenTo.up" (\k n d end -> 0 `smax` (end - (n + k * d)), [])
-                $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up   (k+1) n d end)
-           down = smtFunctionWithMeasure "EnumSymbolic.Float.enumFromThenTo.down" (\k n d end -> 0 `smax` ((n + k * d) - end), [])
-                $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
+-- if x <= z, and the empty list otherwise. We mirror that here.
+enumFromThenToFloat :: SFloat -> SFloat -> SFloat -> SList Float
+enumFromThenToFloat x zIn delta = ite (delta .== 0)
+                                      (ite (x .<= z) (enumFromThen x x) [])
+                                $ ite (delta .>  0) (up 0 x delta z) (down 0 x delta z)
+  where z :: SFloat
+        z = zIn + delta / 2
 
+        -- Unlike the Integer/AlgReal instances, these are NOT given a termination measure:
+        -- floating-point enumeration is genuinely partial. The step @k * d@ can saturate (once
+        -- @k * d@ falls below the ULP of @n@, or once the float @k@ itself stops incrementing),
+        -- so for some inputs @n + k * d@ never exceeds @end@ and the recursion does not terminate
+        -- -- exactly as Haskell's own float enumeration diverges in those cases. A termination
+        -- measure would therefore be unsound: no measure can certify termination of a function
+        -- that does not always terminate. Instead we mark these productive -- each recursive call
+        -- is guarded by a cons, so the definition is well-formed corecursion (finite when the
+        -- enumeration terminates, infinite when it saturates). The d==0 case never reaches here:
+        -- it is routed to the infinite-list branch above.
+        up, down :: SFloat -> SFloat -> SFloat -> SFloat -> SList Float
+        up   = smtProductiveFunction "EnumSymbolic.Float.enumFromThenTo.up"
+             $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up   (k+1) n d end)
+        down = smtProductiveFunction "EnumSymbolic.Float.enumFromThenTo.down"
+             $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
+
 -- | 'EnumSymbolic instance for 'Double'
 instance {-# OVERLAPPING #-} EnumSymbolic Double where
    succ x = x + 1
@@ -1285,23 +1322,33 @@
    toEnum   = sFromIntegral
    fromEnum = fromSDouble sRTZ
 
-   enumFrom   n = enumFromThen   n (n+1)
-   enumFromTo n = enumFromThenTo n (n+1)
+   enumFrom   n   = enumFromThen         n (n+1)
+   enumFromTo n m = enumFromThenToDouble n m 1
 
    enumFromThen x y = go 0 x (y-x)
      where go = smtProductiveFunction "EnumSymbolic.Double.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d
 
-   enumFromThenTo x y zIn = ite (delta .>= 0) (up 0 x delta z) (down 0 x delta z)
-     where delta, z :: SDouble
-           delta = y - x
-           z     = zIn + delta / 2
+   enumFromThenTo x y zIn = enumFromThenToDouble x zIn (y - x)
 
-           up, down :: SDouble -> SDouble -> SDouble -> SDouble -> SList Double
-           up   = smtFunctionWithMeasure "EnumSymbolic.Double.enumFromThenTo.up" (\k n d end -> 0 `smax` (end - (n + k * d)), [])
-                $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up   (k+1) n d end)
-           down = smtFunctionWithMeasure "EnumSymbolic.Double.enumFromThenTo.down" (\k n d end -> 0 `smax` ((n + k * d) - end), [])
-                $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
+-- if x <= z, and the empty list otherwise. We mirror that here.
+enumFromThenToDouble :: SDouble -> SDouble -> SDouble -> SList Double
+enumFromThenToDouble x zIn delta = ite (delta .== 0)
+                                       (ite (x .<= z) (enumFromThen x x) [])
+                                 $ ite (delta .>  0) (up 0 x delta z) (down 0 x delta z)
+  where z :: SDouble
+        z = zIn + delta / 2
 
+        -- See the Float instance for why these are productive rather than measured:
+        -- floating-point enumeration is genuinely partial (the @k * d@ step can saturate), so a
+        -- termination measure would be unsound. Each recursive call is guarded by a cons, so the
+        -- definition is well-formed corecursion. The d==0 case is routed to the branch above.
+        up, down :: SDouble -> SDouble -> SDouble -> SDouble -> SList Double
+        up   = smtProductiveFunction "EnumSymbolic.Double.enumFromThenTo.up"
+             $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up   (k+1) n d end)
+        down = smtProductiveFunction "EnumSymbolic.Double.enumFromThenTo.down"
+             $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
+
 -- | 'EnumSymbolic instance for arbitrary floats
 instance {-# OVERLAPPING #-} ValidFloat eb sb => EnumSymbolic (FloatingPoint eb sb) where
    succ x = x + 1
@@ -1310,23 +1357,33 @@
    toEnum   = sFromIntegral
    fromEnum = fromSFloatingPoint sRTZ
 
-   enumFrom   n = enumFromThen   n (n+1)
-   enumFromTo n = enumFromThenTo n (n+1)
+   enumFrom   n   = enumFromThen                 n (n+1)
+   enumFromTo n m = enumFromThenToFloatingPoint  n m 1
 
    enumFromThen x y = go 0 x (y-x)
      where go = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThen" $ \k n d -> (n + k * d) .: go (k+1) n d
 
-   enumFromThenTo x y zIn = ite (delta .>= 0) (up 0 x delta z) (down 0 x delta z)
-     where delta, z :: SFloatingPoint eb sb
-           delta = y - x
-           z     = zIn + delta / 2
+   enumFromThenTo x y zIn = enumFromThenToFloatingPoint x zIn (y - x)
 
-           up, down :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)
-           up   = smtFunctionWithMeasure "EnumSymbolic.FloatingPoint.enumFromThenTo.up" (\k n d end -> 0 `smax` (end - (n + k * d)), [])
-                $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up   (k+1) n d end)
-           down = smtFunctionWithMeasure "EnumSymbolic.FloatingPoint.enumFromThenTo.down" (\k n d end -> 0 `smax` ((n + k * d) - end), [])
-                $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
+-- if x <= z, and the empty list otherwise. We mirror that here.
+enumFromThenToFloatingPoint :: forall eb sb. ValidFloat eb sb => SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)
+enumFromThenToFloatingPoint x zIn delta = ite (delta .== 0)
+                                              (ite (x .<= z) (enumFromThen x x) [])
+                                        $ ite (delta .>  0) (up 0 x delta z) (down 0 x delta z)
+  where z :: SFloatingPoint eb sb
+        z = zIn + delta / 2
 
+        -- See the Float instance for why these are productive rather than measured:
+        -- floating-point enumeration is genuinely partial (the @k * d@ step can saturate), so a
+        -- termination measure would be unsound. Each recursive call is guarded by a cons, so the
+        -- definition is well-formed corecursion. The d==0 case is routed to the branch above.
+        up, down :: SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SFloatingPoint eb sb -> SList (FloatingPoint eb sb)
+        up   = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThenTo.up"
+             $ \k n d end -> let c = n + k * d in ite (c .> end) [] (c .: up   (k+1) n d end)
+        down = smtProductiveFunction "EnumSymbolic.FloatingPoint.enumFromThenTo.down"
+             $ \k n d end -> let c = n + k * d in ite (c .< end) [] (c .: down (k+1) n d end)
+
 -- | 'EnumSymbolic instance for arbitrary AlgReal. We don't have to use the multiplicative trick here
 -- since alg-reals are precise. But, following rational in Haskell, we do use the stopping point of @z + delta / 2@.
 instance {-# OVERLAPPING #-} EnumSymbolic AlgReal where
@@ -1336,22 +1393,42 @@
    toEnum   = sFromIntegral
    fromEnum = sRealToSIntegerTruncate
 
-   enumFrom   n = enumFromThen   n (n+1)
-   enumFromTo n = enumFromThenTo n (n+1)
+   enumFrom   n   = enumFromThen          n (n+1)
+   enumFromTo n m = enumFromThenToAlgReal n m 1
 
    enumFromThen x y = go x (y-x)
      where go = smtProductiveFunction "EnumSymbolic.AlgReal.enumFromThen" $ \start delta -> start .: go (start+delta) delta
 
-   enumFromThenTo x y zIn = ite (delta .>= 0) (up x delta z) (down x delta z)
-     where delta, z :: SReal
-           delta = y - x
-           z     = zIn + delta / 2
+   enumFromThenTo x y zIn = enumFromThenToAlgReal x zIn (y - x)
 
-           up, down :: SReal -> SReal -> SReal -> SList AlgReal
-           up   = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.up"   (\start _d end -> 0 `smax` (end - start + 1), [])
-                $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up   (start + d) d end)
-           down = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.down" (\start _d end -> 0 `smax` (start - end + 1), [])
-                $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end)
+   enumFromThenToH x y zIn mStep = enumFromThenToAlgReal x zIn (maybe (y - x) fromIntegral mStep)
+
+-- When the step is 0 (i.e., y == x), Haskell produces an infinite list of x's
+-- if x <= z, and the empty list otherwise. We mirror that here.
+enumFromThenToAlgReal :: SReal -> SReal -> SReal -> SList AlgReal
+enumFromThenToAlgReal x zIn delta = ite (delta .== 0)
+                                        (ite (x .<= z) (enumFromThen x x) [])
+                                  $ ite (delta .>  0) (up x delta z) (down x delta z)
+  where z :: SReal
+        z = zIn + delta / 2
+
+        -- The measure is the number of remaining recursive steps, which is an INTEGER:
+        -- @floor ((end - start) / d) + 1@ (clamped at 0). A real-valued measure would be
+        -- unsound here, since the reals are not well-ordered (an infinite descending chain
+        -- like 1, 1/2, 1/4, ... never reaches a minimum). 'sRealToSInteger' is @floor@, and
+        -- @(end - start) / d@ is non-negative in both the up (d>0) and down (d<0) regimes, so
+        -- the same expression serves both.
+        --
+        -- The d==0 case is handled: 'up'/'down' are only *called* with d>0/d<0 (the d==0 case is
+        -- routed to the infinite-list branch above), and for measure *verification* the guard's
+        -- @d .<= 0@/@d .>= 0@ test puts @d>0@/@d<0@ into the reaching condition, so the decrease
+        -- obligation never sees d==0; the @0 `smax`@ keeps non-negativity vacuously true even for
+        -- the unreachable zero-denominator value of @(end - start) / d@.
+        up, down :: SReal -> SReal -> SReal -> SList AlgReal
+        up   = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.up"   (\start d end -> 0 `smax` (sRealToSInteger ((end - start) / d) + 1), [])
+             $ \start d end -> ite (start .> end .|| d .<= 0) [] (start .: up   (start + d) d end)
+        down = smtFunctionWithMeasure "EnumSymbolic.AlgReal.enumFromThenTo.down" (\start d end -> 0 `smax` (sRealToSInteger ((end - start) / d) + 1), [])
+             $ \start d end -> ite (start .< end .|| d .>= 0) [] (start .: down (start + d) d end)
 
 -- | Lookup. If we can't find, then the result is unspecified.
 --
diff --git a/Data/SBV/SEnum.hs b/Data/SBV/SEnum.hs
--- a/Data/SBV/SEnum.hs
+++ b/Data/SBV/SEnum.hs
@@ -39,7 +39,7 @@
 import Data.Char (isSpace)
 
 import Prelude hiding (enumFrom, enumFromThen, enumFromTo, enumFromThenTo)
-import Data.SBV.List  (enumFrom, enumFromThen, enumFromTo, enumFromThenTo)
+import Data.SBV.List  (enumFrom, enumFromThen, enumFromTo, enumFromThenToH)
 
 import Control.Monad (unless)
 import Data.List (isInfixOf, intercalate)
@@ -108,7 +108,13 @@
     ([a],    Nothing) -> varE 'enumFrom       `appE` parseHaskellExpr loc a
     ([a, b], Nothing) -> varE 'enumFromThen   `appE` parseHaskellExpr loc a `appE` parseHaskellExpr loc b
     ([a],    Just c)  -> varE 'enumFromTo     `appE` parseHaskellExpr loc a `appE`                               parseHaskellExpr loc c
-    ([a, b], Just c)  -> varE 'enumFromThenTo `appE` parseHaskellExpr loc a `appE` parseHaskellExpr loc b `appE` parseHaskellExpr loc c
+    ([a, b], Just c)  -> do ea <- parseHaskellExpr loc a
+                            eb <- parseHaskellExpr loc b
+                            ec <- parseHaskellExpr loc c
+                            -- Pass the from/then step as a hint when it's a statically-known integer
+                            -- (e.g. @[m, m-1 .. n]@ => @-1@). Exact-arithmetic instances fold it; the
+                            -- rest ignore it. See 'constStep'.
+                            varE 'enumFromThenToH `appE` pure ea `appE` pure eb `appE` pure ec `appE` liftMStep (constStep ea eb)
 
     _ -> errorWithLoc loc $ unlines [ "Data.SBV.Enum: Invalid format. Use one of:"
                                     , ""
@@ -117,6 +123,50 @@
                                     , "  [sEnum| a    .. c |]"
                                     , "  [sEnum| a, b .. c |]"
                                     ]
+
+-- | Read a parsed expression as @base + offset@: a single opaque atom plus an integer constant.
+-- @Nothing@ base means the whole thing is a pure integer constant. We only look through @+@ and @-@
+-- of integer literals; anything else is treated as an atom. This is intentionally a single-base
+-- peel, not a general linear normalizer -- it's exactly enough to recognize @m@, @m-1@, @m+k@, etc.
+peel :: Exp -> (Maybe Exp, Integer)
+peel (LitE (IntegerL n)) = (Nothing, n)
+peel (ParensE e)         = peel e
+peel (SigE e _)          = peel e
+peel (InfixE  (Just l)               (VarE op) (Just (LitE (IntegerL n)))) = shift op l n
+peel (UInfixE l                      (VarE op)       (LitE (IntegerL n)))   = shift op l n
+peel (InfixE  (Just (LitE (IntegerL n))) (VarE op) (Just r)) | base op == "+" = add (peel r) n
+peel (UInfixE (LitE (IntegerL n))        (VarE op)       r)  | base op == "+" = add (peel r) n
+peel e                   = (Just e, 0)
+
+-- | Helper for 'peel': fold a @base <op> lit@ where @op@ is @+@ or @-@.
+shift :: Name -> Exp -> Integer -> (Maybe Exp, Integer)
+shift op l n = case base op of
+                 "+" -> add (peel l) n
+                 "-" -> add (peel l) (negate n)
+                 _   -> (Just (UInfixE l (VarE op) (LitE (IntegerL n))), 0)
+
+-- | Add a constant to a peeled @(base, offset)@.
+add :: (Maybe Exp, Integer) -> Integer -> (Maybe Exp, Integer)
+add (b, k) n = (b, k + n)
+
+-- | Unqualified name of an operator (haskell-src-meta may leave it unqualified, so compare by base).
+base :: Name -> String
+base = nameBase
+
+-- | The from->then step @then - from@, when it's a statically-known integer (same atom on both
+-- sides, so the atoms cancel). Returns @Nothing@ for genuinely-symbolic steps (distinct atoms),
+-- in which case the quasiquoter falls back to the ordinary, hint-free behavior.
+constStep :: Exp -> Exp -> Maybe Integer
+constStep from thn
+  | bf == bt  = Just (kt - kf)
+  | otherwise = Nothing
+  where (bf, kf) = peel from
+        (bt, kt) = peel thn
+
+-- | Splice a @`Maybe` `Integer`@ step hint into the generated call.
+liftMStep :: Maybe Integer -> Q Exp
+liftMStep Nothing  = conE 'Nothing
+liftMStep (Just n) = conE 'Just `appE` litE (integerL n)
 
 -- | Parses a string into a Haskell TH Exp using haskell-src-meta
 parseHaskellExpr :: Loc -> String -> Q Exp
diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs
--- a/Data/SBV/SMT/SMT.hs
+++ b/Data/SBV/SMT/SMT.hs
@@ -85,7 +85,7 @@
                               )
 
 import Data.SBV.Utils.PrettyNum
-import Data.SBV.Utils.Lib       (joinArgs, splitArgs, needsBars, showText)
+import Data.SBV.Utils.Lib       (joinArgs, splitArgs, needsBars, showText, unQuote)
 import Data.SBV.Utils.SExpr     (parenDeficit, nameSupply)
 
 import qualified System.Timeout as Timeout (timeout)
@@ -773,17 +773,25 @@
           defaultLineTO = Just (scaler defaultLineTimeOut)
 
           -- Default SBVException with solver config baked in; callers override fields as needed
-          solverException desc = SBVException { sbvExceptionDescription = desc
-                                              , sbvExceptionSent        = Nothing
-                                              , sbvExceptionExpected    = Nothing
-                                              , sbvExceptionReceived    = Nothing
-                                              , sbvExceptionStdOut      = Nothing
-                                              , sbvExceptionStdErr      = Nothing
-                                              , sbvExceptionExitCode    = Nothing
-                                              , sbvExceptionConfig      = cfg { solver = (solver cfg) { executable = execPath } }
-                                              , sbvExceptionReason      = Nothing
-                                              , sbvExceptionHint        = Nothing
-                                              }
+          solverException desc =
+             let (errOut, description)
+                    | "(error" `isPrefixOf` desc
+                    = ( Just $ unQuote (dropWhile isSpace (dropWhile (not . isSpace) (init desc)))
+                      , "Unexpected solver error"
+                      )
+                    | True
+                    = (Nothing, desc)
+             in SBVException { sbvExceptionDescription = description
+                             , sbvExceptionSent        = Nothing
+                             , sbvExceptionExpected    = Nothing
+                             , sbvExceptionReceived    = Nothing
+                             , sbvExceptionStdOut      = Nothing
+                             , sbvExceptionStdErr      = errOut
+                             , sbvExceptionExitCode    = Nothing
+                             , sbvExceptionConfig      = cfg { solver = (solver cfg) { executable = execPath } }
+                             , sbvExceptionReason      = Nothing
+                             , sbvExceptionHint        = Nothing
+                             }
 
       (send, ask, getResponseFromSolver, terminateSolver, cleanUp, pid) <- do
                 (inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing
@@ -856,7 +864,11 @@
                                                               pure $ dropWhile isSpace <$> mbCts
 
                                          in case timeOutToUse of
-                                              Nothing -> SolverRegular <$> getFullLine
+                                              Nothing -> do l <- getFullLine
+                                                            -- If we see the line starting with error, we're about to die, so give up:
+                                                            pure $ if "(error" `isPrefixOf` l
+                                                                      then SolverException l
+                                                                      else SolverRegular   l
                                               Just t  -> do r <- Timeout.timeout t getFullLine
                                                             case r of
                                                               Just l  -> pure $ SolverRegular l
diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs
--- a/Data/SBV/SMT/SMTLib2.hs
+++ b/Data/SBV/SMT/SMTLib2.hs
@@ -35,7 +35,7 @@
 
 import Data.SBV.SMT.Utils
 
-import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), getUserName, getUserName', getSV, regExpToSMTString, NROp(..)
+import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), getUserName, getUserName', getSV, regExpToSMTString, NROp(..), showNROp
                               , SMTDef(..), SMTLambda(..), ResultInp(..), ProgInfo(..), SpecialRelOp(..), ADTOp(..)
                               )
 
@@ -917,7 +917,8 @@
 
         sh (SBVApp (NonLinear NR_Pow)  [a, b]) | isZ3 || isCVC5  = "(^  " <> cvtSV a <> " " <> cvtSV b <> ")"
 
-        sh (SBVApp (NonLinear w) args) = "(" <> showText w <> " " <> T.unwords (map cvtSV args) <> ")"
+        sh (SBVApp (NonLinear w) [])   =        T.pack (showNROp (name (solver cfg)) w)
+        sh (SBVApp (NonLinear w) args) = "(" <> T.pack (showNROp (name (solver cfg)) w) <> " " <> T.unwords (map cvtSV args) <> ")"
 
         sh (SBVApp (PseudoBoolean pb) args)
           | hasPB = handlePB pb args'
diff --git a/Data/SBV/Utils/Numeric.hs b/Data/SBV/Utils/Numeric.hs
--- a/Data/SBV/Utils/Numeric.hs
+++ b/Data/SBV/Utils/Numeric.hs
@@ -92,7 +92,7 @@
   | isNaN x      = x
   | x == 0       = x
   | isInfinite x = x
-  | i == 0       = if x < 0 || isNegativeZero x then -0.0 else 0.0
+  | i == 0       = if x < 0 then -0.0 else 0.0
   | True         = fromInteger i
   where i :: Integer
         i = round x
diff --git a/Documentation/SBV/Examples/ADT/Param.hs b/Documentation/SBV/Examples/ADT/Param.hs
--- a/Documentation/SBV/Examples/ADT/Param.hs
+++ b/Documentation/SBV/Examples/ADT/Param.hs
@@ -155,9 +155,9 @@
 -- | Query mode example.
 --
 -- >>> queryE
--- e1: (let h = (-3 * -1) in (1 * h))
+-- e1: (let a = (-3 * (8 + -7)) in ((a * (4 + a)) * -1))
 -- e2: -2
--- e3: (let d = 368 % 369 in d)
+-- e3: (let h = 257 % 258 in h)
 queryE :: IO ()
 queryE = runSMT $ do
            e1 :: SExpr String Integer <- free "e1"
diff --git a/Documentation/SBV/Examples/TP/Basics.hs b/Documentation/SBV/Examples/TP/Basics.hs
--- a/Documentation/SBV/Examples/TP/Basics.hs
+++ b/Documentation/SBV/Examples/TP/Basics.hs
@@ -295,6 +295,37 @@
     r <- prove $ \x -> badM x .== badM x
     print r
 
+-- | A termination measure is only a valid argument for termination if it takes values in a
+-- /well-founded/ order: one with no infinite descending chains. Being non-negative and strictly
+-- decreasing then forces the recursion to stop. The integers (bounded below by @0@) are well-founded,
+-- but the reals are /not/: the chain @1, 1\/2, 1\/4, ...@ descends forever without ever reaching a
+-- minimum. So a real-valued measure proves nothing.
+--
+-- Consider this Zeno-style non-terminating recursion: for any @x > 0@, the argument @x \/ 2@ is
+-- again positive, so it never reaches the base case. Yet the measure @0 `smax` x@ is non-negative
+-- and strictly decreases at the recursive call (@x \/ 2 < x@). Accepting it would mean certifying a
+-- non-terminating function as terminating, which can be used to derive falsehoods.
+--
+-- @
+-- zeno :: SReal -> SReal
+-- zeno = smtFunctionWithMeasure \"zeno\" (\\x -> 0 \`smax\` x, [])
+--      $ \\x -> ite (x .<= 0) 0 (zeno (x \/ 2))
+-- @
+--
+-- SBV rules this out /at compile time/: the 'Data.SBV.Zero' class gates which types may be used as
+-- measures, and there is deliberately no instance for algebraic reals. So the definition above does
+-- not type-check, reporting:
+--
+-- @
+--     • A termination measure may not have a real-valued result.
+--
+--       The reals are not well-ordered: an infinite descending chain such as
+--       1, 1\/2, 1\/4, ... has no least element, so a non-negative and strictly
+--       decreasing real measure does not imply termination.
+--
+--       Use an integer-valued measure instead (e.g. a count of remaining steps).
+-- @
+
 -- * Axioms and consistency
 
 -- | SBV checks that recursive functions defined via 'smtFunction' terminate, verifying a termination measure, which
diff --git a/Documentation/SBV/Examples/TP/Lists.hs b/Documentation/SBV/Examples/TP/Lists.hs
--- a/Documentation/SBV/Examples/TP/Lists.hs
+++ b/Documentation/SBV/Examples/TP/Lists.hs
@@ -375,7 +375,7 @@
 --     Step: 1.2.4                      Q.E.D.
 --     Step: 1.Completeness             Q.E.D.
 --   Result:                            Q.E.D.
--- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up
+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.up
 -- [Proven] enumLen :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
 enumLen :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
 enumLen =
@@ -396,7 +396,7 @@
 --
 -- The proof uses the metric @|m-n|@.
 --
--- >>> runTP $ revNM
+-- >>> runTP revNM
 -- Inductive lemma (strong): helper
 --   Step: Measure is non-negative     Q.E.D.
 --   Step: 1                           Q.E.D.
diff --git a/Documentation/SBV/Examples/TP/Numeric.hs b/Documentation/SBV/Examples/TP/Numeric.hs
--- a/Documentation/SBV/Examples/TP/Numeric.hs
+++ b/Documentation/SBV/Examples/TP/Numeric.hs
@@ -76,8 +76,7 @@
 --   Step: 2                       Q.E.D.
 --   Step: 3                       Q.E.D.
 --   Result:                       Q.E.D.
--- Functions proven terminating:
---   EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up, sbv.foldr
+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr
 -- [Proven] sum_correct :: Ɐn ∷ Integer → Bool
 sumProof :: TP (Proof (Forall "n" Integer -> SBool))
 sumProof = induct "sum_correct"
@@ -103,9 +102,7 @@
 --   Step: 5                             Q.E.D.
 --   Step: 6                             Q.E.D.
 --   Result:                             Q.E.D.
--- Functions proven terminating:
---   EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up,
---   sbv.foldr, sbv.map
+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr, sbv.map
 -- [Proven] sumSquare_correct :: Ɐn ∷ Integer → Bool
 sumSquareProof :: TP (Proof (Forall "n" Integer -> SBool))
 sumSquareProof = do
@@ -155,9 +152,7 @@
 --   Step: 1                       Q.E.D.
 --   Step: 2                       Q.E.D.
 --   Result:                       Q.E.D.
--- Functions proven terminating:
---   EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up,
---   sbv.foldr, sumCubed
+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr, sumCubed
 -- [Proven] nicomachus :: Ɐn ∷ Integer → Bool
 nicomachus :: TP (Proof (Forall "n" Integer -> SBool))
 nicomachus = do
@@ -291,9 +286,7 @@
 --   Step: 6                           Q.E.D.
 --   Step: 7                           Q.E.D.
 --   Result:                           Q.E.D.
--- Functions proven terminating:
---   EnumSymbolic.Integer.enumFromThenTo.down, EnumSymbolic.Integer.enumFromThenTo.up,
---   sbv.foldr, sbv.map
+-- Functions proven terminating: EnumSymbolic.Integer.enumFromThenTo.down, sbv.foldr, sbv.map
 -- [Proven] sumMulFactorial :: Ɐn ∷ Integer → Bool
 sumMulFactorial :: TP (Proof (Forall "n" Integer -> SBool))
 sumMulFactorial = do
diff --git a/SBVTestSuite/GoldFiles/adt_gen00.gold b/SBVTestSuite/GoldFiles/adt_gen00.gold
--- a/SBVTestSuite/GoldFiles/adt_gen00.gold
+++ b/SBVTestSuite/GoldFiles/adt_gen00.gold
@@ -267,11 +267,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (Let "y"
-            (Add (Val (- 2)) (Mul (Val (- 1)) (Val 3)))
-            (Let "a" (Val 13) (Add (Add (Val (- 3)) (Val 2)) (Var "a"))))))
+[RECV] ((s0 (Let "m"
+            (Add (Val 1) (Mul (Val (- 2)) (Val 0)))
+            (Let "k" (Val 11) (Add (Add (Val (- 1)) (Val 2)) (Var "k"))))))
 
-Got: (let y = (-2 + (-1 * 3)) in (let a = 13 in ((-3 + 2) + a)))
+Got: (let m = (1 + (-2 * 0)) in (let k = 11 in ((-1 + 2) + k)))
 DONE
 *** Solver   : Z3
 *** Exit code: ExitSuccess
diff --git a/SBVTestSuite/GoldFiles/adt_pgen00.gold b/SBVTestSuite/GoldFiles/adt_pgen00.gold
--- a/SBVTestSuite/GoldFiles/adt_pgen00.gold
+++ b/SBVTestSuite/GoldFiles/adt_pgen00.gold
@@ -267,11 +267,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (Let "s"
-            (Let "i" (Val 1) (Mul (Val 2) (Add (Var "i") (Var "i"))))
-            (Let "a" (Val 9) (Add (Val 3) (Var "a"))))))
+[RECV] ((s0 (Let "l"
+            (Let "n" (Val (- 1)) (Mul (Val (- 2)) (Add (Var "n") (Var "n"))))
+            (Let "d" (Val 4) (Add (Add (Var "d") (Var "d")) (Var "d"))))))
 
-Got: (let s = (let i = 1 in (2 * (i + i))) in (let a = 9 in (3 + a)))
+Got: (let l = (let n = -1 in (-2 * (n + n))) in (let d = 4 in ((d + d) + d)))
 DONE
 *** Solver   : Z3
 *** Exit code: ExitSuccess
diff --git a/SBVTestSuite/GoldFiles/exceptionLocal1.gold b/SBVTestSuite/GoldFiles/exceptionLocal1.gold
--- a/SBVTestSuite/GoldFiles/exceptionLocal1.gold
+++ b/SBVTestSuite/GoldFiles/exceptionLocal1.gold
@@ -48,17 +48,11 @@
 [GOOD] (define-fun s31 () (_ BitVec 32) (bvmul s30 s30))
 [GOOD] (define-fun s32 () (_ BitVec 32) (bvmul s31 s31))
 [GOOD] (define-fun s33 () (_ BitVec 32) (bvmul s32 s32))
-[FAIL] (define-fun s34 () (_ BitVec 32) (bvmul s33 s33))
 CAUGHT SMT EXCEPTION
-*** Data.SBV: Unexpected non-success response from Yices:
+*** Data.SBV: Unexpected solver error:
 ***
 ***    Sent      : (define-fun s34 () (_ BitVec 32) (bvmul s33 s33))
-***    Expected  : success
-***    Received  : (error "at line 40, column 35: in bvmul: maximal polynomial degree exceeded")
 ***
-***    Exit code : ExitSuccess
+***    Stderr    : at line 40, column 35: in bvmul: maximal polynomial degree exceeded
 ***    Executable: /usr/local/bin/yices-smt2
 ***    Options   : --incremental
-***
-***    Reason    : Check solver response for further information. If your code is correct,
-***                please report this as an issue either with SBV or the solver itself!
diff --git a/SBVTestSuite/GoldFiles/exceptionLocal2.gold b/SBVTestSuite/GoldFiles/exceptionLocal2.gold
--- a/SBVTestSuite/GoldFiles/exceptionLocal2.gold
+++ b/SBVTestSuite/GoldFiles/exceptionLocal2.gold
@@ -11,17 +11,11 @@
 [GOOD] ; --- literal constants ---
 [GOOD] (define-fun s1 () Real (/ 2.0 1.0))
 [GOOD] ; --- top level inputs ---
-[FAIL] (declare-fun s0 () Real) ; tracks user variable "x"
 CAUGHT SMT EXCEPTION
-*** Data.SBV: Unexpected non-success response from Z3:
+*** Data.SBV: Unexpected solver error:
 ***
 ***    Sent      : (declare-fun s0 () Real) ; tracks user variable "x"
-***    Expected  : success
-***    Received  : (error "line 8 column 23: logic does not support reals")
 ***
-***    Exit code : ExitFailure (-15)
+***    Stderr    : line 8 column 23: logic does not support reals
 ***    Executable: /usr/local/bin/z3
 ***    Options   : -nw -in -smt2
-***
-***    Reason    : Check solver response for further information. If your code is correct,
-***                please report this as an issue either with SBV or the solver itself!
diff --git a/SBVTestSuite/GoldFiles/exceptionRemote1.gold b/SBVTestSuite/GoldFiles/exceptionRemote1.gold
--- a/SBVTestSuite/GoldFiles/exceptionRemote1.gold
+++ b/SBVTestSuite/GoldFiles/exceptionRemote1.gold
@@ -1,3 +1,3 @@
 
-FINAL: "OK, we got: Unexpected response from the solver, context: assert"
+FINAL: "OK, we got: Unexpected solver error"
 DONE!
diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr
--- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr
+++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr
@@ -15,8 +15,8 @@
        (isLet e ==> (e .== e =: qed))]
 PCase17.hs:18:14: error: [GHC-83865]
     " Couldn't match expected type: Proof SBool
-                  with actual type: sbv-14.2:Data.SBV.TP.TP.TPProofGen
-                                      (SBV Bool) [sbv-14.2:Data.SBV.TP.TP.Helper] ()
+                  with actual type: sbv-14.3:Data.SBV.TP.TP.TPProofGen
+                                      (SBV Bool) [sbv-14.3:Data.SBV.TP.TP.Helper] ()
     " In the expression:
         cases
           [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)),
diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr
--- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr
+++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr
@@ -15,8 +15,8 @@
        (isLet e ==> undefined)]
 PCase38.hs:12:14: error: [GHC-83865]
     " Couldn't match expected type: Proof SBool
-                  with actual type: sbv-14.2:Data.SBV.TP.TP.TPProofGen
-                                      a0 [sbv-14.2:Data.SBV.TP.TP.Helper] ()
+                  with actual type: sbv-14.3:Data.SBV.TP.TP.TPProofGen
+                                      a0 [sbv-14.3:Data.SBV.TP.TP.Helper] ()
     " In the expression:
         cases
           [(isZero e ==> undefined), (isNum e ==> undefined),
diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr
--- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr
+++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr
@@ -28,4 +28,4 @@
          ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m))
          (ite
             (Data.SBV.Maybe.isNothing m) 0
-            (symWithKind "unmatched_sCase_Maybe_6989586621679034958")))
+            (symWithKind "unmatched_sCase_Maybe_6989586621679035004")))
diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr
--- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr
+++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr
@@ -24,4 +24,4 @@
                ((\ _ -> Data.SBV.Either.isRight (Data.SBV.Maybe.getJust_1 m))
                   (Data.SBV.Maybe.getJust_1 m)))
             ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m))
-            (symWithKind "unmatched_sCase_Maybe_6989586621679034958")))
+            (symWithKind "unmatched_sCase_Maybe_6989586621679035004")))
diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr
--- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr
+++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr
@@ -30,4 +30,4 @@
          (ite
             (Data.SBV.Either.isRight e)
             ((\ _ -> 1) (Data.SBV.Either.getRight_1 e))
-            (symWithKind "unmatched_sCase_Either_6989586621679034920")))
+            (symWithKind "unmatched_sCase_Either_6989586621679034966")))
diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr
--- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr
+++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr
@@ -40,4 +40,4 @@
                   (isVar e) ((\ _ -> 1) (getVar_1 e))
                   (ite
                      (isLet e) ((\ _ _ _ -> 3) (getLet_1 e) (getLet_2 e) (getLet_3 e))
-                     (symWithKind "unmatched_sCase_Expr_6989586621679081453"))))))
+                     (symWithKind "unmatched_sCase_Expr_6989586621679081499"))))))
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,7 +1,7 @@
 Cabal-Version: 2.2
 
 Name        : sbv
-Version     : 14.2
+Version     : 14.3
 Category    : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
 Synopsis    : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
 Description : Express properties about Haskell programs and automatically prove them using SMT