diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,54 @@
 * Hackage: <http://hackage.haskell.org/package/sbv>
 * GitHub:  <http://leventerkok.github.com/sbv/>
 
-* Latest Hackage released version: 7.8, 2018-05-18
+* Latest Hackage released version: 7.9, 2018-06-15
+
+### Version 7.9, 2018-06-15
+ 
+  * Add support for bit-vector arithmetic underflow/overflow detection. The new
+    'ArithmeticOverflow' class captures conditions under which addition, subtraction,
+    multiplication, division, and negation can underflow/overflow for
+    both signed and unsigned bit-vector values. The implementation is based on
+    http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf,
+    and can be used to detect overflow caused bugs in machine arithmetic.
+    See "Data.SBV.Tools.Overflow" for details.
+
+  * Add 'sFromIntegralO', which is the overflow/underflow detecting variant
+    of 'sFromIntegral'. This function returns (along with the converted
+    result), a pair of booleans showing whether the conversion underflowed
+    or overflowed.
+
+  * Change the function 'getUnknownReason' to return a proper data-type
+    ('SMTReasonUnknown') as opposed to a mere string. This is at the
+    query level. Similarly, change `Unknown` result to return the same
+    data-type at the sat/prove level.
+
+  * Interpolants: With Z3 4.8.0 release, Z3 folks have dropped support
+    for producing interpolants. If you need interpolants, you will have
+    to use the MathSAT backend now. Also, the MathSAT API is slightly
+    different from how Z3 supported interpolants as well, which means
+    your old code will need some modifications. See the example in
+    Documentation.SBV.Examples.Queries.Interpolants for the new usage.
+
+  * Add 'constrainWithAttribute' call, which can be used to attach 
+    arbitrary attribute to a constraint. Main use case is in interpolant
+    generation with MathSAT.
+
+  * C code generation: SBV now spits out linker flag -lm if needed.
+    Thanks to Matt Peddie for reporting.
+
+  * Code reorg: Simplify constant mapping table, by properly accounting
+    for negative-zero floats.
+    
+  * Export 'sexprToVal' for the class SMTValue, which allows for custom
+    definitions of value extractions. Thanks to Brian Schroeder for the
+    patch.
+  
+  * Export 'Logic' directly from Data.SBV. (Previously was from Control.)
+
+  * Fix a long standing issue (ever since we introduced queries) where
+    'sAssert' calls were run in the context of the final output boolean,
+    which is simply the wrong thing to do.
 
 ### Version 7.8, Released 2018-05-18
 
diff --git a/Data/SBV.hs b/Data/SBV.hs
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -209,9 +209,9 @@
   -- ** Constraint Vacuity
   -- $constraintVacuity
 
-  -- ** Named constraints
+  -- ** Named constraints and attributes
   -- $namedConstraints
-  , namedConstraint
+  , namedConstraint, constrainWithAttribute
 
   -- ** Unsat cores
   -- $unsatCores
@@ -247,7 +247,7 @@
 
   -- ** Inspecting proof results
   -- $resultTypes
-  , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
+  , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..), SMTReasonUnknown(..)
 
   -- ** Observing expressions
   -- $observeInternal
@@ -267,7 +267,7 @@
   , boolector, cvc4, yices, z3, mathSAT, abc
   -- ** Configurations
   , defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers
-  , setLogic, setOption, setInfo, setTimeOut
+  , setLogic, Logic(..), setOption, setInfo, setTimeOut
   -- ** Solver exceptions
   , SMTException(..)
 
@@ -309,7 +309,8 @@
 import Data.Generics
 
 import Data.SBV.SMT.Utils (SMTException(..))
-import Data.SBV.Control.Utils (SMTValue)
+import Data.SBV.Control.Utils (SMTValue (..))
+import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))
 
 -- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing
 -- problems with constraints, like the following:
@@ -591,11 +592,16 @@
     * ['Pareto']. Finally, the user can query for pareto-fronts. A pareto front is an model such that no goal can be made
       "better" without making some other goal "worse."
 
+      Pareto fronts only make sense when the objectives are bounded. If there are unbounded objective values, then the
+      backend solver can loop infinitely. (This is what z3 does currently.) If you are not sure the objectives are
+      bounded, you should first use 'Independent' mode to ensure the objectives are bounded, and then switch to
+      pareto-mode to extract them further.
+
       The optional number argument to 'Pareto' specifies the maximum number of pareto-fronts the user is asking
-      to get. If 'Nothing', SBV will query for all pareto-fronts. Note that pareto-fronts can be infinite
-      in number, so if 'Nothing' is used, there is a potential for infinitely waiting for the SBV-solver interaction
-      to finish. (If you suspect this might be the case, run in 'verbose' mode to see the interaction and
-      put a limiting factor appropriately.)
+      to get. If 'Nothing', SBV will query for all pareto-fronts. Note that pareto-fronts can be really large,
+      so if 'Nothing' is used, there is a potential for waiting indefinitely for the SBV-solver interaction to finish. (If
+      you suspect this might be the case, run in 'verbose' mode to see the interaction and put a limiting factor
+      appropriately.)
 -}
 
 {- $softAssertions
@@ -826,6 +832,12 @@
 Constraints can be given names:
 
   @ 'namedConstraint' "a is at least 5" $ a .>= 5@
+
+Similarly, arbitrary term attributes can also be associated:
+
+  @ 'constrainWithAttribute' [(":solver-specific-attribute", "value")] $ a .>= 5@
+
+Note that a 'namedConstraint' is equivalent to a 'constrainWithAttribute' call, setting the `":named"' attribute.
 -}
 
 {- $unsatCores
diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs
--- a/Data/SBV/Compilers/C.hs
+++ b/Data/SBV/Compilers/C.hs
@@ -104,13 +104,18 @@
                                , (nmd ++ ".c", (CgDriver,         genDriver cfg randVals nm ins outs mbRet))
                                , (nm  ++ ".c", (CgSource,         body))
                                ]
-        body = genCProg cfg nm sig sbvProg ins outs mbRet extDecls
+
+        (body, flagsNeeded) = genCProg cfg nm sig sbvProg ins outs mbRet extDecls
+
         bundleKind = (cgInteger cfg, cgReal cfg)
+
         randVals = cgDriverVals cfg
+
         filt xs  = [c | c@(_, (k, _)) <- xs, need k]
           where need k | isCgDriver   k = cgGenDriver cfg
                        | isCgMakefile k = cgGenMakefile cfg
                        | True           = True
+
         nmd      = nm ++ "_driver"
         sig      = pprCFunHeader nm ins outs mbRet
         ins      = cgInputs st
@@ -126,7 +131,7 @@
         extDecls  = case cgDecls st of
                      [] -> empty
                      xs -> vcat $ text "/* User given declarations: */" : map text xs
-        flags    = cgLDFlags st
+        flags    = flagsNeeded ++ cgLDFlags st
 
 -- | Pretty print a functions type. If there is only one output, we compile it
 -- as a function that returns that value. Otherwise, we compile it as a void function
@@ -411,7 +416,7 @@
                         spec      = specifier cfg sw
 
 -- | Generate the C program
-genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]
+genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> ([Doc], [String])
 genCProg cfg fn proto (Result kindInfo _tvals _ovals cgs ins preConsts tbls arrs _uis _axioms (SBVPgm asgns) cstrs origAsserts _) inVars outVars mbRet extDecls
   | isNothing (cgInteger cfg) && KUnbounded `Set.member` kindInfo
   = error $ "SBV->C: Unbounded integers are not supported by the C compiler."
@@ -432,7 +437,7 @@
   | needsExistentials (map fst (fst ins))
   = error "SBV->C: Cannot compile functions with existentially quantified variables."
   | True
-  = [pre, header, post]
+  = ([pre, header, post], flagsNeeded)
  where asserts | cgIgnoreAsserts cfg = []
                | True                = origAsserts
 
@@ -462,6 +467,10 @@
 
        assignments = F.toList asgns
 
+       -- Do we need any linker flags for C?
+       flagsNeeded = nub $ concatMap (getLDFlag . opRes) assignments
+          where opRes (sw, SBVApp o _) = (o, kindOf sw)
+
        codeSeg (fnm, ls) =  text "/* User specified custom code for" <+> doubleQuotes (text fnm) <+> text "*/"
                          $$ vcat (map text ls)
                          $$ text ""
@@ -687,6 +696,7 @@
         p (Label s)        [a] = a <+> text "/*" <+> text s <+> text "*/"
         p (IEEEFP w)         as = handleIEEE w  consts (zip opArgs as) var
         p (PseudoBoolean pb) as = handlePB pb as
+        p (OverflowOp o) _      = tbd $ "Overflow operations" ++ show o
         p (KindCast _ to)   [a] = parens (text (show to)) <+> a
         p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s
         p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s P.<> parens (fsep (punctuate comma as))
@@ -949,5 +959,32 @@
                  ptag = "printf(\"" ++ tag ++ "\\n\");"
                  lsep = replicate (length tag) '='
                  psep = "printf(\"" ++ lsep ++ "\\n\");"
+
+-- Does this operation with this result kind require an LD flag?
+getLDFlag :: (Op, Kind) -> [String]
+getLDFlag (o, k) = flag o
+  where math = ["-lm"]
+
+        flag (IEEEFP FP_Cast{})                                     = math
+        flag (IEEEFP fop)       | fop `elem` requiresMath           = math
+        flag Abs                | k `elem` [KFloat, KDouble, KReal] = math
+        flag _                                                      = []
+
+        requiresMath = [ FP_Abs
+                       , FP_FMA
+                       , FP_Sqrt
+                       , FP_Rem
+                       , FP_Min
+                       , FP_Max
+                       , FP_RoundToIntegral
+                       , FP_ObjEqual
+                       , FP_IsSubnormal
+                       , FP_IsInfinite
+                       , FP_IsNaN
+                       , FP_IsNegative
+                       , FP_IsPositive
+                       , FP_IsNormal
+                       , FP_IsZero
+                       ]
 
 {-# ANN module ("HLint: ignore Redundant lambda" :: String) #-}
diff --git a/Data/SBV/Compilers/CodeGen.hs b/Data/SBV/Compilers/CodeGen.hs
--- a/Data/SBV/Compilers/CodeGen.hs
+++ b/Data/SBV/Compilers/CodeGen.hs
@@ -295,7 +295,7 @@
 data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
 
 -- | Different kinds of "files" we can produce. Currently this is quite "C" specific.
-data CgPgmKind = CgMakefile [String]
+data CgPgmKind = CgMakefile [String]  -- list of flags to pass to linker
                | CgHeader [Doc]
                | CgSource
                | CgDriver
diff --git a/Data/SBV/Control.hs b/Data/SBV/Control.hs
--- a/Data/SBV/Control.hs
+++ b/Data/SBV/Control.hs
@@ -40,7 +40,7 @@
      , getAssertions
 
      -- * Getting solver information
-     , SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..)
+     , SMTInfoFlag(..), SMTErrorBehavior(..), SMTInfoResponse(..)
      , getInfo, getOption
 
      -- * Entering and exiting assertion stack
@@ -69,15 +69,11 @@
 
      -- * Solver options
      , SMTOption(..)
-
-     -- * Logics supported
-     , Logic(..)
-
      ) where
 
 import Data.SBV.Core.Data     (SMTProblem(..), SMTSolver(..), SMTConfig(..))
 import Data.SBV.Core.Symbolic ( Query, IStage(..), SBVRunMode(..), Symbolic, Query(..), rSMTOptions
-                              , extractSymbolicSimulationState, solverSetOptions, runMode
+                              , extractSymbolicSimulationState, solverSetOptions, runMode, isRunIStage
                               )
 
 import Data.SBV.Control.Query
@@ -96,12 +92,14 @@
      rm <- liftIO $ readIORef (runMode st)
      case rm of
         -- Transitioning from setup
-        SMTMode ISetup isSAT cfg -> liftIO $ do let backend = engine (solver cfg)
+        SMTMode stage isSAT cfg | not (isRunIStage stage) -> liftIO $ do
 
+                                                let backend = engine (solver cfg)
+
                                                 res     <- extractSymbolicSimulationState st
                                                 setOpts <- reverse <$> readIORef (rSMTOptions st)
 
-                                                let SMTProblem{smtLibPgm} = runProofOn cfg isSAT [] res
+                                                let SMTProblem{smtLibPgm} = runProofOn rm [] res
                                                     cfg' = cfg { solverSetOptions = solverSetOptions cfg ++ setOpts }
                                                     pgm  = smtLibPgm cfg'
 
diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs
--- a/Data/SBV/Control/Query.hs
+++ b/Data/SBV/Control/Query.hs
@@ -38,6 +38,7 @@
 import qualified Data.Map    as M
 import qualified Data.IntMap as IM
 
+import Data.Char     (toLower)
 import Data.List     (unzip3, intercalate, nubBy, sortBy)
 import Data.Maybe    (listToMaybe, catMaybes)
 import Data.Function (on)
@@ -110,8 +111,6 @@
 
         isAllStat = isAllStatistics flag
 
-        render = serialize True
-
         grabAllStat k v = (render k, render v)
 
         -- we're trying to do our best to get key-value pairs here, but this
@@ -134,13 +133,25 @@
                  EApp [ECon ":error-behavior", ECon "immediate-exit"]      -> return $ Resp_Error ErrorImmediateExit
                  EApp [ECon ":error-behavior", ECon "continued-execution"] -> return $ Resp_Error ErrorContinuedExecution
                  EApp (ECon ":name" : o)                                   -> return $ Resp_Name (render (EApp o))
-                 EApp [ECon ":reason-unknown", ECon "memout"]              -> return $ Resp_ReasonUnknown UnknownMemOut
-                 EApp [ECon ":reason-unknown", ECon "incomplete"]          -> return $ Resp_ReasonUnknown UnknownIncomplete
-                 EApp (ECon ":reason-unknown" : o)                         -> return $ Resp_ReasonUnknown (UnknownOther (render (EApp o)))
+                 EApp (ECon ":reason-unknown" : o)                         -> return $ Resp_ReasonUnknown (unk o)
                  EApp (ECon ":version" : o)                                -> return $ Resp_Version (render (EApp o))
                  EApp (ECon s : o)                                         -> return $ Resp_InfoKeyword s (map render o)
                  _                                                         -> bad r Nothing
 
+  where render = serialize True
+
+        unk [ECon s] | Just d <- getUR s = d
+        unk o                            = UnknownOther (render (EApp o))
+
+        getUR s = map toLower (unQuote s) `lookup` [(map toLower k, d) | (k, d) <- unknownReasons]
+
+        -- As specified in Section 4.1 of the SMTLib document. Note that we're adding the
+        -- extra timeout as it is useful in this context.
+        unknownReasons = [ ("memout",     UnknownMemOut)
+                         , ("incomplete", UnknownIncomplete)
+                         , ("timeout",    UnknownTimeOut)
+                         ]
+
 -- | Retrieve the value of an 'SMTOption.' The curious function argument is on purpose here,
 -- simply pass the constructor name. Example: the call @'getOption' 'ProduceUnsatCores'@ will return
 -- either @Nothing@ or @Just (ProduceUnsatCores True)@ or @Just (ProduceUnsatCores False)@.
@@ -186,16 +197,13 @@
         stringList c e _ = return $ Just $ c $ stringsOf e
 
 -- | Get the reason unknown. Only internally used.
-getUnknownReason :: Query String
+getUnknownReason :: Query SMTReasonUnknown
 getUnknownReason = do ru <- getInfo ReasonUnknown
                       case ru of
-                        Resp_Unsupported     -> return "No reason provided."
-                        Resp_ReasonUnknown r -> return $ case r of
-                                                           UnknownMemOut       -> "Out of memory."
-                                                           UnknownIncomplete   -> "Incomplete."
-                                                           UnknownOther      s -> s
+                        Resp_Unsupported     -> return $ UnknownOther "Solver responded: Unsupported."
+                        Resp_ReasonUnknown r -> return r
                         -- Shouldn't happen, but just in case:
-                        _                    -> return $ "Unexpected reason value received: " ++ show ru
+                        _                    -> error $ "Unexpected reason value received: " ++ show ru
 
 -- | Issue check-sat and get an SMT Result out.
 getSMTResult :: Query SMTResult
@@ -254,7 +262,7 @@
                                     Unsat -> return (False, [])
                                     Sat   -> continue (classifyModel cfg)
                                     Unk   -> do ur <- getUnknownReason
-                                                return (False, [ProofError cfg [ur]])
+                                                return (False, [ProofError cfg [show ur]])
 
   where continue classify = do m <- getModel
                                (limReached, fronts) <- getParetoFronts (subtract 1 <$> mbN) [m]
@@ -623,13 +631,13 @@
         -- result of parsing is ignored.
         parse r bad $ \_ -> return r
 
--- | Retrieve interpolants after an 'Unsat' result is obtained. Note you must have arranged for
+-- | Retrieve an interpolant after an 'Unsat' result is obtained. Note you must have arranged for
 -- interpolants to be produced first (/via/ @'setOption' $ 'ProduceInterpolants' 'True'@)
 -- for this call to not error out!
 --
--- To get an interpolant for a pair of formulas @A@ and @B@, use a 'namedConstraint' to attach
--- names to @A@ and @B@. Then call 'getInterpolant' @[\"A\", \"B\"]@, assuming those are the names
--- you gave to the formulas.
+-- To get an interpolant for a pair of formulas @A@ and @B@, use a 'constrainWithAttribute' call to attach
+-- interplation groups to @A@ and @B@. Then call 'getInterpolant' @[\"A\"]@, assuming those are the names
+-- you gave to the formulas in the @A@ group.
 --
 -- An interpolant for @A@ and @B@ is a formula @I@ such that:
 --
@@ -643,35 +651,28 @@
 -- be satisfied at the same time. Furthermore, @I@ will have only the symbols that are common
 -- to @A@ and @B@.
 --
--- Interpolants generalize to sequences: If you pass more than two formulas, then you will get
--- a sequence of interpolants. In general, for @N@ formulas that are not satisfiable together, you will be
--- returned @N-1@ interpolants. If formulas are @A1 .. An@, then interpolants will be @I1 .. I(N-1)@, such
--- that @A1 ==> I1@, @A2 /\\ I1 ==> I2@, @A3 /\\ I2 ==> I3@, ..., and finally @AN ===> not I(N-1)@.
---
--- Currently, SBV only returns simple and sequence interpolants, and does not support tree-interpolants.
--- If you need these, please get in touch. Furthermore, the result will be a list of mere strings representing the
--- interpolating formulas, as opposed to a more structured type. Please get in touch if you use this function and can
--- suggest a better API.
-getInterpolant :: [String] -> Query [String]
+-- N.B. As of Z3 version 4.8.0; Z3 no longer supports interpolants. Use the MathSAT backend for extracting
+-- interpolants. See 'Documentation.SBV.Examples.Queries.Interpolants' for an example.
+getInterpolant :: [String] -> Query String
 getInterpolant fs
-  | length fs < 2
-  = error $ "SBV.getInterpolant requires at least two named constraints, received: " ++ show fs
+  | null fs
+  = error "SBV.getInterpolant requires at least one marked constraint, received none!"
   | True
   = do let bar s = '|' : s ++ "|"
-           cmd = "(get-interpolant " ++ unwords (map bar fs) ++ ")"
+           cmd = "(get-interpolant (" ++ unwords (map bar fs) ++ "))"
            bad = unexpected "getInterpolant" cmd "a get-interpolant response"
                           $ Just [ "Make sure you use:"
                                  , ""
                                  , "       setOption $ ProduceInterpolants True"
                                  , ""
                                  , "to make sure the solver is ready for producing interpolants,"
-                                 , "and that you have named the formulas with calls to 'namedConstraint'."
+                                 , "and that you have used the proper attributes using the"
+                                 , "constrainWithAttribute function."
                                  ]
 
        r <- ask cmd
 
-       parse r bad $ \case EApp (ECon "interpolants" : es) -> return $ map (serialize False) es
-                           _                               -> bad r Nothing
+       parse r bad $ \e -> return $ serialize False e
 
 -- | Retrieve assertions. Note you must have arranged for
 -- assertions to be available first (/via/ @'setOption' $ 'ProduceAssertions' 'True'@)
diff --git a/Data/SBV/Control/Types.hs b/Data/SBV/Control/Types.hs
--- a/Data/SBV/Control/Types.hs
+++ b/Data/SBV/Control/Types.hs
@@ -51,8 +51,16 @@
 -- | Reason for reporting unknown.
 data SMTReasonUnknown = UnknownMemOut
                       | UnknownIncomplete
+                      | UnknownTimeOut
                       | UnknownOther      String
-                      deriving Show
+                      deriving (Generic, NFData)
+
+-- | Show instance for unknown
+instance Show SMTReasonUnknown where
+  show UnknownMemOut     = "memout"
+  show UnknownIncomplete = "incomplete"
+  show UnknownTimeOut    = "timeout"
+  show (UnknownOther s)  = s
 
 -- | Collectable information from the solver.
 data SMTInfoResponse = Resp_Unsupported
diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs
--- a/Data/SBV/Control/Utils.hs
+++ b/Data/SBV/Control/Utils.hs
@@ -60,15 +60,15 @@
                               , QueryState(..), SVal(..), Quantifier(..), cache
                               , newExpr, SBVExpr(..), Op(..), FPOp(..), SBV(..)
                               , SolverContext(..), SBool, Objective(..), SolverCapabilities(..), capabilities
-                              , Result(..), SMTProblem(..), trueSW, SymWord(..), SBVPgm(..), SMTSolver(..)
+                              , Result(..), SMTProblem(..), trueSW, SymWord(..), SBVPgm(..), SMTSolver(..), SBVRunMode(..)
                               )
-import Data.SBV.Core.Symbolic (IncState(..), withNewIncState, State(..), svToSW, registerLabel, svMkSymVar)
+import Data.SBV.Core.Symbolic (IncState(..), withNewIncState, State(..), svToSW, registerLabel, svMkSymVar, isSafetyCheckingIStage, isSetupIStage)
 
 import Data.SBV.Core.AlgReals   (mergeAlgReals)
 import Data.SBV.Core.Operations (svNot, svNotEqual, svOr)
 
 import Data.SBV.SMT.SMTLib  (toIncSMTLib, toSMTLib)
-import Data.SBV.SMT.Utils   (showTimeoutValue, annotateWithName, alignPlain, debug, mergeSExpr, SMTException(..))
+import Data.SBV.SMT.Utils   (showTimeoutValue, addAnnotations, alignPlain, debug, mergeSExpr, SMTException(..))
 
 import Data.SBV.Utils.Lib (qfsToString)
 
@@ -83,8 +83,9 @@
 
 -- | 'Query' as a 'SolverContext'.
 instance SolverContext Query where
-   constrain          = addQueryConstraint Nothing
-   namedConstraint nm = addQueryConstraint (Just nm)
+   constrain                 = addQueryConstraint []
+   namedConstraint nm        = addQueryConstraint [(":named", nm)]
+   constrainWithAttribute    = addQueryConstraint
 
    setOption o
      | isStartModeOption o = error $ unlines [ ""
@@ -93,15 +94,12 @@
                                              ]
      | True                = send True $ setSMTOption o
 
--- | Adding a constraint, possibly named. Only used internally.
+-- | Adding a constraint, possibly with attributes. Only used internally.
 -- Use 'constrain' and 'namedConstraint' from user programs.
-addQueryConstraint :: Maybe String -> SBool -> Query ()
-addQueryConstraint mbNm b = do sw <- inNewContext (\st -> do maybe (return ()) (registerLabel st) mbNm
+addQueryConstraint :: [(String, String)] -> SBool -> Query ()
+addQueryConstraint atts b = do sw <- inNewContext (\st -> do mapM_ (registerLabel st) [nm | (":named", nm) <- atts]
                                                              sbvToSW st b)
-                               send True $ "(assert " ++ mkNamed mbNm (show sw)  ++ ")"
-   where mkNamed Nothing   s = s
-         mkNamed (Just nm) s = annotateWithName nm s
-
+                               send True $ "(assert " ++ addAnnotations atts (show sw)  ++ ")"
 
 -- | Get the current configuration
 getConfig :: Query SMTConfig
@@ -131,12 +129,11 @@
 syncUpSolver afterAPush is = do
         cfg <- getConfig
         ls  <- io $ do let swap  (a, b)        = (b, a)
-                           swapc ((_, a), b)   = (b, a)
                            cmp   (a, _) (b, _) = a `compare` b
                            arrange (i, (at, rt, es)) = ((i, at, rt), es)
                        inps  <- reverse <$> readIORef (rNewInps is)
                        ks    <- readIORef (rNewKinds is)
-                       cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rNewConsts is)
+                       cnsts <- sortBy cmp . map swap . Map.toList <$> readIORef (rNewConsts is)
                        arrs  <- IMap.toAscList <$> readIORef (rNewArrs is)
                        tbls  <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef (rNewTbls is)
                        uis   <- Map.toAscList <$> readIORef (rNewUIs is)
@@ -680,9 +677,13 @@
         io $ C.throwIO exc
 
 -- | Convert a query result to an SMT Problem
-runProofOn :: SMTConfig -> Bool -> [String] -> Result -> SMTProblem
-runProofOn config isSat comments res@(Result ki _qcInfo _observables _codeSegs is consts tbls arrs uis axs pgm cstrs _assertions outputs) =
-     let flipQ (ALL, x) = (EX,  x)
+runProofOn :: SBVRunMode -> [String] -> Result -> SMTProblem
+runProofOn rm comments res@(Result ki _qcInfo _observables _codeSegs is consts tbls arrs uis axs pgm cstrs _assertions outputs) =
+     let (config, isSat, isSafe, isSetup) = case rm of
+                                              SMTMode stage s c -> (c, s, isSafetyCheckingIStage stage, isSetupIStage stage)
+                                              _                 -> error $ "runProofOn: Unexpected run mode: " ++ show rm
+
+         flipQ (ALL, x) = (EX,  x)
          flipQ (EX,  x) = (ALL, x)
 
          skolemize :: [(Quantifier, NamedSymVar)] -> [Either SW (SW, [SW])]
@@ -694,23 +695,18 @@
          qinps      = if isSat then fst is else map flipQ (fst is)
          skolemMap  = skolemize qinps
 
-         o = case outputs of
-               []  -> trueSW
-               [so] -> case so of
-                        SW KBool _ -> so
-                        _          -> trueSW
-                                      {-
-                                      -- TODO: We used to error out here, but "safeWith" might have a non-bool out
-                                      -- I wish we can get rid of this and still check for it. Perhaps this entire
-                                      -- runProofOn might disappear.
-                                      error $ unlines [ "Impossible happened, non-boolean output: " ++ show so
-                                                      , "Detected while generating the trace:\n" ++ show res
-                                                      ]
-                                      -}
-               os  -> error $ unlines [ "User error: Multiple output values detected: " ++ show os
-                                      , "Detected while generating the trace:\n" ++ show res
-                                      , "*** Check calls to \"output\", they are typically not needed!"
-                                      ]
+         o | isSafe = trueSW
+           | True   = case outputs of
+                        []  | isSetup -> trueSW
+                        [so]          -> case so of
+                                           SW KBool _ -> so
+                                           _          -> error $ unlines [ "Impossible happened, non-boolean output: " ++ show so
+                                                                         , "Detected while generating the trace:\n" ++ show res
+                                                                         ]
+                        os  -> error $ unlines [ "User error: Multiple output values detected: " ++ show os
+                                               , "Detected while generating the trace:\n" ++ show res
+                                               , "*** Check calls to \"output\", they are typically not needed!"
+                                               ]
 
      in SMTProblem { smtLibPgm = toSMTLib config ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o }
 
diff --git a/Data/SBV/Core/Concrete.hs b/Data/SBV/Core/Concrete.hs
--- a/Data/SBV/Core/Concrete.hs
+++ b/Data/SBV/Core/Concrete.hs
@@ -24,6 +24,8 @@
 import Data.SBV.Core.Kind
 import Data.SBV.Core.AlgReals
 
+import Data.SBV.Utils.Numeric (fpIsEqualObjectH, fpCompareObjectH)
+
 -- | A constant value
 data CWVal = CWAlgReal  !AlgReal              -- ^ algebraic real
            | CWInteger  !Integer              -- ^ bit-vector/unbounded integer
@@ -37,14 +39,14 @@
 -- instances for these when values are infinitely precise reals. However, we do
 -- need a structural eq/ord for Map indexes; so define custom ones here:
 instance Eq CWVal where
-  CWAlgReal a  == CWAlgReal b  = a `algRealStructuralEqual` b
-  CWInteger a  == CWInteger b  = a == b
-  CWUserSort a == CWUserSort b = a == b
-  CWFloat a    == CWFloat b    = a == b
-  CWDouble a   == CWDouble b   = a == b
-  CWChar   a   == CWChar b     = a == b
-  CWString a   == CWString b   = a == b
-  _            == _            = False
+  CWAlgReal  a   == CWAlgReal  b = a `algRealStructuralEqual` b
+  CWInteger  a   == CWInteger  b = a == b
+  CWUserSort a   == CWUserSort b = a == b
+  CWFloat    a   == CWFloat    b = a `fpIsEqualObjectH` b   -- We don't want +0/-0 to be confused; and also we want NaN = NaN here!
+  CWDouble   a   == CWDouble   b = a `fpIsEqualObjectH` b   -- ditto
+  CWChar     a   == CWChar     b = a == b
+  CWString   a   == CWString   b = a == b
+  _              == _            = False
 
 -- | Ord instance for CWVal. Same comments as the 'Eq' instance why this cannot be derived.
 instance Ord CWVal where
@@ -66,7 +68,7 @@
 
   CWFloat _   `compare`  CWAlgReal _  = GT
   CWFloat _   `compare`  CWInteger _  = GT
-  CWFloat a   `compare`  CWFloat b    = a `compare` b
+  CWFloat a   `compare`  CWFloat b    = a `fpCompareObjectH` b
   CWFloat _   `compare`  CWDouble _   = LT
   CWFloat _   `compare`  CWChar _     = LT
   CWFloat _   `compare`  CWString _   = LT
@@ -75,7 +77,7 @@
   CWDouble _  `compare`  CWAlgReal _  = GT
   CWDouble _  `compare`  CWInteger _  = GT
   CWDouble _  `compare`  CWFloat _    = GT
-  CWDouble a  `compare`  CWDouble b   = a `compare` b
+  CWDouble a  `compare`  CWDouble b   = a `fpCompareObjectH` b
   CWDouble _  `compare`  CWChar _     = LT
   CWDouble _  `compare`  CWString _   = LT
   CWDouble _  `compare`  CWUserSort _ = LT
diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs
--- a/Data/SBV/Core/Data.hs
+++ b/Data/SBV/Core/Data.hs
@@ -264,6 +264,8 @@
    constrain       :: SBool -> m ()
    -- | Add a named constraint. The name is used in unsat-core extraction.
    namedConstraint :: String -> SBool -> m ()
+   -- | Add a constraint, with arbitrary attributes. Used in interpolant generation.
+   constrainWithAttribute :: [(String, String)] -> SBool -> m ()
    -- | Set info. Example: @setInfo ":status" ["unsat"]@.
    setInfo :: String -> [String] -> m ()
    -- | Set an option.
diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs
--- a/Data/SBV/Core/Floating.hs
+++ b/Data/SBV/Core/Floating.hs
@@ -389,7 +389,7 @@
                              newExpr st w32 (SBVApp (IEEEFP (FP_Reinterpret KFloat w32)) [f])
                      else do n   <- internalVariable st w32
                              ysw <- newExpr st KFloat (SBVApp (IEEEFP (FP_Reinterpret w32 KFloat)) [n])
-                             internalConstraint st Nothing $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KFloat (Right (cache (\_ -> return ysw))))
+                             internalConstraint st [] $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KFloat (Right (cache (\_ -> return ysw))))
                              return n
 
 -- | Convert an 'SDouble' to an 'SWord64', preserving the bit-correspondence. Note that since the
@@ -410,7 +410,7 @@
                              newExpr st w64 (SBVApp (IEEEFP (FP_Reinterpret KDouble w64)) [f])
                      else do n   <- internalVariable st w64
                              ysw <- newExpr st KDouble (SBVApp (IEEEFP (FP_Reinterpret w64 KDouble)) [n])
-                             internalConstraint st Nothing $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KDouble (Right (cache (\_ -> return ysw))))
+                             internalConstraint st [] $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KDouble (Right (cache (\_ -> return ysw))))
                              return n
 
 -- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have
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
@@ -1779,9 +1779,11 @@
 
 -- | Symbolic computations provide a context for writing symbolic programs.
 instance SolverContext Symbolic where
-   constrain          (SBV c) = imposeConstraint Nothing   c
-   namedConstraint nm (SBV c) = imposeConstraint (Just nm) c
-   setOption o                = addNewSMTOption  o
+   constrain                   (SBV c) = imposeConstraint []               c
+   namedConstraint        nm   (SBV c) = imposeConstraint [(":named", nm)] c
+   constrainWithAttribute atts (SBV c) = imposeConstraint atts             c
+
+   setOption o = addNewSMTOption  o
 
 -- | Introduce a soft assertion, with an optional penalty
 assertSoft :: String -> SBool -> Penalty -> Symbolic ()
diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs
--- a/Data/SBV/Core/Operations.hs
+++ b/Data/SBV/Core/Operations.hs
@@ -31,6 +31,8 @@
   , svSelect
   , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE
   , svExp, svFromIntegral
+  -- ** Overflows
+  , svMkOverflow
   -- ** Derived operations
   , svToWord1, svFromWord1, svTestBit
   , svShiftLeft, svShiftRight
@@ -49,7 +51,6 @@
 import Data.SBV.Core.Kind
 import Data.SBV.Core.Concrete
 import Data.SBV.Core.Symbolic
-import Data.SBV.Utils.Numeric (fpIsEqualObjectH)
 
 import Data.Ratio
 
@@ -487,13 +488,8 @@
   = a
   | True
   = SVal k $ Right $ cache c
-  where
-        -- Be careful with +/-0 here! See https://github.com/LeventErkok/sbv/issues/382
-        sameResult (SVal _ (Left c1)) (SVal _ (Left c2)) = c1 == c2 && floatCheck (cwVal c1) (cwVal c2)
-        sameResult _                       _             = False
-        floatCheck (CWFloat  f1) (CWFloat  f2)           = f1 `fpIsEqualObjectH` f2
-        floatCheck (CWDouble d1) (CWDouble d2)           = d1 `fpIsEqualObjectH` d2
-        floatCheck _            _                        = True
+  where sameResult (SVal _ (Left c1)) (SVal _ (Left c2)) = c1 == c2
+        sameResult _                  _                  = False
 
         c st = do swt <- svToSW st t
                   case () of
@@ -802,6 +798,14 @@
           z  = svInteger (kindOf x) 0
           zi = svInteger (kindOf i) 0
           n  = svInteger (kindOf i) (toInteger sx)
+
+--------------------------------------------------------------------------------
+-- | Overflow detection.
+svMkOverflow :: OvOp -> SVal -> SVal -> SVal
+svMkOverflow o x y = SVal KBool (Right (cache r))
+    where r st = do sx <- svToSW st x
+                    sy <- svToSW st y
+                    newExpr st KBool $ SBVApp (OverflowOp o) [sx, sy]
 
 --------------------------------------------------------------------------------
 -- Utility functions
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
@@ -27,7 +27,7 @@
 module Data.SBV.Core.Symbolic
   ( NodeId(..)
   , SW(..), swKind, trueSW, falseSW
-  , Op(..), PBOp(..), FPOp(..), StrOp(..), RegExp(..)
+  , Op(..), PBOp(..), OvOp(..), FPOp(..), StrOp(..), RegExp(..)
   , Quantifier(..), needsExistentials
   , RoundingMode(..)
   , SBVType(..), newUninterpreted, addAxiom
@@ -35,7 +35,7 @@
   , svMkSymVar, sWordN, sWordN_, sIntN, sIntN_
   , ArrayContext(..), ArrayInfo
   , svToSW, svToSymSW, forceSWArg
-  , SBVExpr(..), newExpr, isCodeGenMode
+  , SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage
   , Cached, cache, uncache
   , ArrayIndex, uncacheAI
   , NamedSymVar
@@ -64,7 +64,7 @@
 import Data.Char                (isAlpha, isAlphaNum, toLower)
 import Data.IORef               (IORef, newIORef, readIORef)
 import Data.List                (intercalate, sortBy)
-import Data.Maybe               (isJust, fromJust, fromMaybe)
+import Data.Maybe               (isJust, fromJust, fromMaybe, listToMaybe)
 import Data.String              (IsString(fromString))
 
 import Data.Time (getCurrentTime, UTCTime)
@@ -154,6 +154,7 @@
         | Label String                          -- Essentially no-op; useful for code generation to emit comments.
         | IEEEFP FPOp                           -- Floating-point ops, categorized separately
         | PseudoBoolean PBOp                    -- Pseudo-boolean ops, categorized separately
+        | OverflowOp    OvOp                    -- Overflow-ops, categorized separately
         | StrOp StrOp                           -- String ops, categorized separately
         deriving (Eq, Ord)
 
@@ -221,6 +222,18 @@
           | PB_Eq      [Int] Int  -- ^ Exactly k,  with coefficients given. Generalized PB_Exactly
           deriving (Eq, Ord, Show)
 
+-- | Overflow operations
+data OvOp = Overflow_SMul_OVFL   -- ^ Signed multiplication overflow
+          | Overflow_SMul_UDFL   -- ^ Signed multiplication underflow
+          | Overflow_UMul_OVFL   -- ^ Unsigned multiplication overflow
+          deriving (Eq, Ord)
+
+-- | Show instance. It's important that these follow the internal z3 names
+instance Show OvOp where
+  show Overflow_SMul_OVFL = "bvsmul_noovfl"
+  show Overflow_SMul_UDFL = "bvsmul_noudfl"
+  show Overflow_UMul_OVFL = "bvumul_noovfl"
+
 -- | String operations. Note that we do not define `StrAt` as it translates to `StrSubStr` trivially.
 data StrOp = StrConcat       -- ^ Concatenation of one or more strings
            | StrLen          -- ^ String length
@@ -339,6 +352,7 @@
   show (Label s)         = "[label] " ++ s
   show (IEEEFP w)        = show w
   show (PseudoBoolean p) = show p
+  show (OverflowOp o)    = show o
   show (StrOp s)         = show s
   show op
     | Just s <- op `lookup` syms = s
@@ -392,6 +406,7 @@
   show (SBVApp (Rol i) [a])               = unwords [show a, "<<<", show i]
   show (SBVApp (Ror i) [a])               = unwords [show a, ">>>", show i]
   show (SBVApp (PseudoBoolean pb) args)   = unwords (show pb : map show args)
+  show (SBVApp (OverflowOp op)    args)   = unwords (show op : map show args)
   show (SBVApp op                 [a, b]) = unwords [show a, show op, show b]
   show (SBVApp op                 args)   = unwords (show op : map show args)
 
@@ -406,7 +421,7 @@
 -- potentially be an infinite number of them and there is no way to know exactly
 -- how many ahead of time. If 'Nothing' is given, SBV will possibly loop forever
 -- if the number is really infinite.
-data OptimizeStyle = Lexicographic      -- ^ Objectives are optimized in the order given, earlier objectives have higher priority. This is the default.
+data OptimizeStyle = Lexicographic      -- ^ Objectives are optimized in the order given, earlier objectives have higher priority.
                    | Independent        -- ^ Each objective is optimized independently.
                    | Pareto (Maybe Int) -- ^ Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse.
                    deriving (Eq, Show)
@@ -470,7 +485,7 @@
                      , resUIConsts    :: [(String, SBVType)]                              -- ^ uninterpreted constants
                      , resAxioms      :: [(String, [String])]                             -- ^ axioms
                      , resAsgns       :: SBVPgm                                           -- ^ assignments
-                     , resConstraints :: [(Maybe String, SW)]                             -- ^ additional constraints (boolean)
+                     , resConstraints :: [([(String, String)], SW)]                       -- ^ additional constraints (boolean)
                      , resAssertions  :: [(String, Maybe CallStack, SW)]                  -- ^ assertions
                      , resOutputs     :: [SW]                                             -- ^ outputs
                      }
@@ -540,8 +555,9 @@
 
           shax (nm, ss) = "  -- user defined axiom: " ++ nm ++ "\n  " ++ intercalate "\n  " ss
 
-          shCstr (Nothing, c) = show c
-          shCstr (Just nm, c) = nm ++ ": " ++ show c
+          shCstr ([], c)               = show c
+          shCstr ([(":named", nm)], c) = nm ++ ": " ++ show c
+          shCstr (attrs, c)            = show c ++ " (attributes: " ++ show attrs ++ ")"
 
           shAssert (nm, stk, p) = "  -- assertion: " ++ nm ++ " " ++ maybe "[No location]"
 #if MIN_VERSION_base(4,9,0)
@@ -562,16 +578,16 @@
   show (ArrayMerge  s i j) = " merged arrays " ++ show i ++ " and " ++ show j ++ " on condition " ++ show s
 
 -- | Expression map, used for hash-consing
-type ExprMap   = Map.Map SBVExpr SW
+type ExprMap = Map.Map SBVExpr SW
 
--- | Constants are stored in a map, for hash-consing. The bool is needed to tell -0 from +0, sigh
-type CnstMap   = Map.Map (Bool, CW) SW
+-- | Constants are stored in a map, for hash-consing.
+type CnstMap = Map.Map CW SW
 
 -- | Kinds used in the program; used for determining the final SMT-Lib logic to pick
 type KindSet = Set.Set Kind
 
 -- | Tables generated during a symbolic run
-type TableMap  = Map.Map (Kind, Kind, [SW]) Int
+type TableMap = Map.Map (Kind, Kind, [SW]) Int
 
 -- | Representation for symbolic arrays
 type ArrayInfo = (String, (Kind, Kind), ArrayContext)
@@ -589,9 +605,31 @@
 type Cache a   = IMap.IntMap [(StableName (State -> IO a), a)]
 
 -- | Stage of an interactive run
-data IStage = ISetup    -- Before we initiate contact
-            | IRun      -- After the contact is started
+data IStage = ISetup        -- Before we initiate contact.
+            | ISafe         -- In the context of a safe/safeWith call
+            | IRun          -- After the contact is started
 
+-- | Are we cecking safety
+isSafetyCheckingIStage :: IStage -> Bool
+isSafetyCheckingIStage s = case s of
+                             ISetup -> False
+                             ISafe  -> True
+                             IRun   -> False
+
+-- | Are we in setup?
+isSetupIStage :: IStage -> Bool
+isSetupIStage s = case s of
+                   ISetup -> True
+                   ISafe  -> False
+                   IRun   -> True
+
+-- | Are we in a run?
+isRunIStage :: IStage -> Bool
+isRunIStage s = case s of
+                  ISetup -> False
+                  ISafe  -> False
+                  IRun   -> True
+
 -- | Different means of running a symbolic piece of code
 data SBVRunMode = SMTMode  IStage Bool SMTConfig -- ^ In regular mode, with a stage. Bool is True if this is SAT.
                 | CodeGen                        -- ^ Code generation mode.
@@ -600,8 +638,10 @@
 -- Show instance for SBVRunMode; debugging purposes only
 instance Show SBVRunMode where
    show (SMTMode ISetup True  _) = "Satisfiability setup"
+   show (SMTMode ISafe  True  _) = "Safety setup"
    show (SMTMode IRun   True  _) = "Satisfiability"
    show (SMTMode ISetup False _) = "Proof setup"
+   show (SMTMode ISafe  False _) = error "ISafe-False is not an expected/supported combination for SBVRunMode!"
    show (SMTMode IRun   False _) = "Proof"
    show CodeGen                  = "Code generation"
    show Concrete                 = "Concrete evaluation"
@@ -665,7 +705,7 @@
                     , rUsedKinds   :: IORef KindSet
                     , rUsedLbls    :: IORef (Set.Set String)
                     , rinps        :: IORef ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- User defined, and internal existential
-                    , rConstraints :: IORef [(Maybe String, SW)]
+                    , rConstraints :: IORef [([(String, String)], SW)]
                     , routs        :: IORef [SW]
                     , rtblMap      :: IORef TableMap
                     , spgm         :: IORef SBVPgm
@@ -856,24 +896,16 @@
           else modifyState st rUsedLbls (Set.insert nm) (return ())
 
 -- | Create a new constant; hash-cons as necessary
--- NB. For each constant, we also store weather it's negative-0 or not,
--- as otherwise +0 == -0 and thus we'd confuse those entries. That's a
--- bummer as we incur an extra boolean for this rare case, but it's simple
--- and hopefully we don't generate a ton of constants in general.
 newConst :: State -> CW -> IO SW
 newConst st c = do
   constMap <- readIORef (rconstMap st)
-  let key = (isNeg0 (cwVal c), c)
-  case key `Map.lookup` constMap of
+  case c `Map.lookup` constMap of
     Just sw -> return sw
     Nothing -> do let k = kindOf c
                   (sw, _) <- newSW st k
-                  let ins = Map.insert key sw
+                  let ins = Map.insert c sw
                   modifyState st rconstMap ins $ modifyIncState st rNewConsts ins
                   return sw
-  where isNeg0 (CWFloat  f) = isNegativeZero f
-        isNeg0 (CWDouble d) = isNegativeZero d
-        isNeg0 _            = False
 {-# INLINE newConst #-}
 
 -- | Create a new table; hash-cons as necessary
@@ -1102,21 +1134,24 @@
    SBVPgm rpgm  <- readIORef pgm
    inpsO <- (reverse *** reverse) <$> readIORef inps
    outsO <- reverse <$> readIORef outs
+
    let swap  (a, b)              = (b, a)
-       swapc ((_, a), b)         = (b, a)
        cmp   (a, _) (b, _)       = a `compare` b
        arrange (i, (at, rt, es)) = ((i, at, rt), es)
-   cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rconstMap st)
+
+   cnsts <- sortBy cmp . map swap . Map.toList <$> readIORef (rconstMap st)
    tbls  <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef tables
    arrs  <- IMap.toAscList <$> readIORef arrays
    unint <- Map.toList <$> readIORef uis
    axs   <- reverse <$> readIORef axioms
    knds  <- readIORef usedKinds
    cgMap <- Map.toList <$> readIORef cgs
-   traceVals  <- reverse <$> readIORef cInfo
+
+   traceVals   <- reverse <$> readIORef cInfo
    observables <- reverse <$> readIORef observes
-   extraCstrs <- reverse <$> readIORef cstrs
-   assertions <- reverse <$> readIORef asserts
+   extraCstrs  <- reverse <$> readIORef cstrs
+   assertions  <- reverse <$> readIORef asserts
+
    return $ Result knds traceVals observables cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO
 
 -- | Add a new option
@@ -1125,23 +1160,21 @@
                         liftIO $ modifyState st rSMTOptions (o:) (return ())
 
 -- | Handling constraints
-imposeConstraint :: Maybe String -> SVal -> Symbolic ()
-imposeConstraint mbNm c = do st <- ask
-                             rm <- liftIO $ readIORef (runMode st)
-                             case rm of
-                               CodeGen -> error "SBV: constraints are not allowed in code-generation"
-                               _       -> do () <- case mbNm of
-                                                     Nothing -> return ()
-                                                     Just nm -> liftIO $ registerLabel st nm
-                                             liftIO $ internalConstraint st mbNm c
+imposeConstraint :: [(String, String)] -> SVal -> Symbolic ()
+imposeConstraint attrs c = do st <- ask
+                              rm <- liftIO $ readIORef (runMode st)
+                              case rm of
+                                CodeGen -> error "SBV: constraints are not allowed in code-generation"
+                                _       -> liftIO $ do mapM_ (registerLabel st) [nm | (":named",  nm) <- attrs]
+                                                       internalConstraint st attrs c
 
 -- | Require a boolean condition to be true in the state. Only used for internal purposes.
-internalConstraint :: State -> Maybe String -> SVal -> IO ()
-internalConstraint st mbNm b = do v <- svToSW st b
-                                  modifyState st rConstraints ((mbNm, v):)
-                                            $ noInteractive [ "Adding an internal constraint:"
-                                                            , "  Named: " ++ fromMaybe "<unnamed>" mbNm
-                                                            ]
+internalConstraint :: State -> [(String, String)] -> SVal -> IO ()
+internalConstraint st attrs b = do v <- svToSW st b
+                                   modifyState st rConstraints ((attrs, v):)
+                                             $ noInteractive [ "Adding an internal constraint:"
+                                                             , "  Named: " ++ fromMaybe "<unnamed>" (listToMaybe [nm | (":named", nm) <- attrs])
+                                                             ]
 
 -- | Add an optimization goal
 addSValOptGoal :: Objective SVal -> Symbolic ()
@@ -1439,7 +1472,7 @@
 data SMTResult = Unsatisfiable SMTConfig (Maybe [String]) -- ^ Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter.
                | Satisfiable   SMTConfig SMTModel         -- ^ Satisfiable with model
                | SatExtField   SMTConfig SMTModel         -- ^ Prover returned a model, but in an extension field containing Infinite/epsilon
-               | Unknown       SMTConfig String           -- ^ Prover returned unknown, with the given reason
+               | Unknown       SMTConfig SMTReasonUnknown -- ^ Prover returned unknown, with the given reason
                | ProofError    SMTConfig [String]         -- ^ Prover errored out
 
 -- | A script, to be passed to the solver.
@@ -1476,3 +1509,4 @@
 
 {-# ANN type FPOp ("HLint: ignore Use camelCase" :: String) #-}
 {-# ANN type PBOp ("HLint: ignore Use camelCase" :: String) #-}
+{-# ANN type OvOp ("HLint: ignore Use camelCase" :: String) #-}
diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs
--- a/Data/SBV/Provers/Prover.hs
+++ b/Data/SBV/Provers/Prover.hs
@@ -378,7 +378,7 @@
 
         (_, res) <- runSymbolic (SMTMode ISetup isSat cfg) $ (if isSat then forSome_ else forAll_) a >>= output
 
-        let SMTProblem{smtLibPgm} = Control.runProofOn cfg isSat comments res
+        let SMTProblem{smtLibPgm} = Control.runProofOn (SMTMode IRun isSat cfg) comments res
             out                   = show (smtLibPgm cfg)
 
         return $ out ++ "\n(check-sat)\n"
@@ -559,7 +559,7 @@
                        let mkRelative path
                               | cwd `isPrefixOf` path = drop (length cwd) path
                               | True                  = path
-                       fst <$> runSymbolic (SMTMode ISetup True cfg) (sName_ a >> check mkRelative)
+                       fst <$> runSymbolic (SMTMode ISafe True cfg) (sName_ a >> check mkRelative)
      where check mkRelative = Control.query $ Control.getSBVAssertions >>= mapM (verify mkRelative)
 
            -- check that the cond is unsatisfiable. If satisfiable, that would
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
@@ -156,8 +156,8 @@
                ParetoResult (False, [r]) -> sh (\s -> "Unique pareto front: " ++ s) r
                ParetoResult (False, rs)  -> multi "pareto optimal values" (zipWith shP [(1::Int)..] rs)
                ParetoResult (True,  rs)  ->    multi "pareto optimal values" (zipWith shP [(1::Int)..] rs)
-                                           ++ "\n*** Note: Pareto-front extraction was terminated before stream was ended as requested by the user."
-                                           ++ "\n***       There might be other (potentially infinitely more) results."
+                                           ++ "\n*** Note: Pareto-front extraction was terminated as requested by the user."
+                                           ++ "\n***       There might be many other results!"
 
        where multi w [] = "There are no " ++ w ++ " to display models for."
              multi _ xs = intercalate "\n" xs
@@ -385,7 +385,7 @@
   getModelAssignment (Unsatisfiable _ _) = Left "SBV.getModelAssignment: Unsatisfiable result"
   getModelAssignment (Satisfiable _ m)   = Right (False, parseModelOut m)
   getModelAssignment (SatExtField _ _)   = Left "SBV.getModelAssignment: The model is in an extension field"
-  getModelAssignment (Unknown _ m)       = Left $ "SBV.getModelAssignment: Solver state is unknown: " ++ m
+  getModelAssignment (Unknown _ m)       = Left $ "SBV.getModelAssignment: Solver state is unknown: " ++ show m
   getModelAssignment (ProofError _ s)    = error $ unlines $ "Backend solver complains: " : s
 
   modelExists Satisfiable{}   = True
@@ -428,7 +428,7 @@
   Satisfiable _ (SMTModel _ []) -> satMsg
   Satisfiable _ m               -> satMsgModel ++ showModel cfg m
   SatExtField _ (SMTModel b _)  -> satExtMsg   ++ showModelDictionary cfg b
-  Unknown     _ r               -> unkMsg ++ ".\n" ++ "  Reason: " `alignPlain` r
+  Unknown     _ r               -> unkMsg ++ ".\n" ++ "  Reason: " `alignPlain` show r
   ProofError  _ []              -> "*** An error occurred. No additional information available. Try running in verbose mode"
   ProofError  _ ls              -> "*** An error occurred.\n" ++ intercalate "\n" (map ("***  " ++) ls)
  where cfg = resultConfig result
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
@@ -14,6 +14,7 @@
 
 import Data.Bits  (bit)
 import Data.List  (intercalate, partition, unzip3)
+import Data.Maybe (listToMaybe, fromMaybe)
 
 import qualified Data.Foldable as F (toList)
 import qualified Data.Map      as M
@@ -168,15 +169,16 @@
 
         finalAssert
           | null foralls
-          = map (\a -> "(assert " ++ named a ++ ")") assertions
+          = map (\a -> "(assert " ++ uncurry addAnnotations a ++ ")") assertions
           | not (null namedAsserts)
-          = error $ intercalate "\n" [ "SBV: Named constraints and quantifiers cannot be mixed!"
+          = error $ intercalate "\n" [ "SBV: Constraints with attributes and quantifiers cannot be mixed!"
                                      , "   Quantified variables: " ++ unwords (map show foralls)
                                      , "   Named constraints   : " ++ intercalate ", " (map show namedAsserts)
                                      ]
           | True
           = [impAlign (letShift combined) ++ replicate noOfCloseParens ')']
-          where namedAsserts = [n | (Just n, _) <- assertions]
+          where namedAsserts = [findName attrs | (attrs, _) <- assertions, not (null attrs)]
+                 where findName attrs = fromMaybe "<anonymous>" (listToMaybe [nm | (":named", nm) <- attrs])
 
                 combined = case map snd assertions of
                              [x] -> x
@@ -202,12 +204,12 @@
         --     -- negation of the output in a prove
         --     -- output itself in a sat
         assertions
-           | null finals = [(Nothing, cvtSW skolemMap trueSW)]
+           | null finals = [([], cvtSW skolemMap trueSW)]
            | True        = finals
 
-           where finals  = cstrs' ++ maybe [] (\r -> [(Nothing, r)]) mbO
+           where finals  = cstrs' ++ maybe [] (\r -> [([], r)]) mbO
 
-                 cstrs' =  [(mbNm, c') | (mbNm, c) <- cstrs, Just c' <- [pos c]]
+                 cstrs' =  [(attrs, c') | (attrs, c) <- cstrs, Just c' <- [pos c]]
 
                  mbO | isSat = pos out
                      | True  = neg out
@@ -606,7 +608,7 @@
                                , (Join, lift2 "concat")
                                ]
 
-        sh (SBVApp (Label m) [a]) = curry named (Just m) $ cvtSW skolemMap a  -- This won't be reached; but just in case!
+        sh (SBVApp (Label _) [a]) = cvtSW skolemMap a  -- This won't be reached; but just in case!
 
         sh (SBVApp (IEEEFP (FP_Cast kFrom kTo m)) args) = handleFPCast kFrom kTo (ssw m) (unwords (map ssw args))
         sh (SBVApp (IEEEFP w                    ) args) = "(" ++ show w ++ " " ++ unwords (map ssw args) ++ ")"
@@ -616,6 +618,9 @@
           | True       = reducePB pb args'
           where args' = map ssw args
 
+        -- NB: Z3 semantics have the predicates reversed: i.e., it returns true if overflow isn't possible. Hence the not.
+        sh (SBVApp (OverflowOp op) args) = "(not (" ++ show op ++ " " ++ unwords (map ssw args) ++ "))"
+
         -- Note the unfortunate reversal in StrInRe..
         sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in.re " ++ unwords (map ssw args) ++ " " ++ show r ++ ")"
         sh (SBVApp (StrOp op)          args) = "(" ++ show op ++ " " ++ unwords (map ssw args) ++ ")"
@@ -865,8 +870,3 @@
 
   where addIf :: [Int] -> String
         addIf cs = "(+ " ++ unwords ["(ite " ++ a ++ " " ++ show c ++ " 0)" | (a, c) <- zip args cs] ++ ")"
-
--- Add a named annotation
-named :: (Maybe String, String) -> String
-named (Nothing, x) = x
-named (Just nm, x) = annotateWithName nm x
diff --git a/Data/SBV/SMT/Utils.hs b/Data/SBV/SMT/Utils.hs
--- a/Data/SBV/SMT/Utils.hs
+++ b/Data/SBV/SMT/Utils.hs
@@ -14,7 +14,7 @@
 module Data.SBV.SMT.Utils (
           SMTLibConverter
         , SMTLibIncConverter
-        , annotateWithName
+        , addAnnotations
         , showTimeoutValue
         , alignDiagnostic
         , alignPlain
@@ -46,7 +46,7 @@
                        -> [(String, SBVType)]                           -- ^ uninterpreted functions/constants
                        -> [(String, [String])]                          -- ^ user given axioms
                        -> SBVPgm                                        -- ^ assignments
-                       -> [(Maybe String, SW)]                          -- ^ extra constraints
+                       -> [([(String, String)], SW)]                    -- ^ extra constraints
                        -> SW                                            -- ^ output variable
                        -> SMTConfig                                     -- ^ configuration
                        -> a
@@ -62,10 +62,12 @@
                           -> SMTConfig                   -- ^ configuration
                           -> a
 
--- | Create an annotated term with the given name
-annotateWithName :: String -> String -> String
-annotateWithName nm x = "(! " ++ x ++ " :named |" ++ concatMap sanitize nm ++ "|)"
-  where sanitize '|'  = "_bar_"
+-- | Create an annotated term
+addAnnotations :: [(String, String)] -> String -> String
+addAnnotations []   x = x
+addAnnotations atts x = "(! " ++ x ++ " " ++ unwords (map mkAttr atts) ++ ")"
+  where mkAttr (a, v) = a ++ " |" ++ concatMap sanitize v ++ "|"
+        sanitize '|'  = "_bar_"
         sanitize '\\' = "_backslash_"
         sanitize c    = [c]
 
diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs
--- a/Data/SBV/String.hs
+++ b/Data/SBV/String.hs
@@ -138,7 +138,7 @@
         y si st = do c <- internalVariable st w8
                      cs <- newExpr st KString (SBVApp (StrOp StrUnit) [c])
                      let csSBV = SBV (SVal KString (Right (cache (\_ -> return cs))))
-                     internalConstraint st Nothing $ unSBV $ csSBV .== si
+                     internalConstraint st [] $ unSBV $ csSBV .== si
                      return c
 
 -- | Short cut for 'strToCharAt'
diff --git a/Data/SBV/Tools/Overflow.hs b/Data/SBV/Tools/Overflow.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Tools/Overflow.hs
@@ -0,0 +1,399 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Tools.Overflow
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Implementation of overflow detection functions.
+-- Based on: <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf>
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE Rank2Types           #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Data.SBV.Tools.Overflow (
+
+         -- * Arithmetic overflows
+         ArithOverflow(..)
+
+         -- * Cast overflows
+       , sFromIntegralO
+
+    ) where
+
+import Data.SBV.Core.Data
+import Data.SBV.Core.Symbolic
+import Data.SBV.Core.Model
+import Data.SBV.Core.Operations
+import Data.SBV.Utils.Boolean
+
+-- Doctest only
+-- $setup
+-- >>> import Data.SBV.Provers.Prover (prove, allSat)
+-- >>> import Data.SBV.Utils.Boolean ((<=>))
+
+-- | Detecting underflow/overflow conditions. For each function,
+-- the first result is the condition under which the computation
+-- underflows, and the second is the condition under which it
+-- overflows.
+class ArithOverflow a where
+  -- | Bit-vector addition. Unsigned addition can only overflow. Signed addition can underflow and overflow.
+  --
+  -- A tell tale sign of unsigned addition overflow is when the sum is less than minumum of the arguments.
+  --
+  -- >>> prove $ \x y -> snd (bvAddO x (y::SWord16)) <=> x + y .< x `smin` y
+  -- Q.E.D.
+  bvAddO :: a -> a -> (SBool, SBool)
+
+  -- | Bit-vector subtraction. Unsigned subtraction can only underflow. Signed subtraction can underflow and overflow.
+  bvSubO :: a -> a -> (SBool, SBool)
+
+  -- | Bit-vector multiplication. Unsigned multiplication can only overflow. Signed multiplication can underflow and overflow.
+  bvMulO     :: a -> a -> (SBool, SBool)
+
+  -- | Same as 'bvMulO', except instead of doing the computation internally, it simply sends it off to z3 as a primitive.
+  -- Obviously, only use if you have the z3 backend! Note that z3 provides this operation only when no logic is set,
+  -- so make sure to call @setLogic Logic_NONE@ in your program!
+  bvMulOFast :: a -> a -> (SBool, SBool)
+
+  -- | Bit-vector division. Unsigned division neither underflows nor overflows. Signed division can only overflow. In fact, for each
+  -- signed bitvector type, there's precisely one pair that overflows, when @x@ is @minBound@ and @y@ is @-1@:
+  --
+  -- >>> allSat $ \x y -> snd (x `bvDivO` (y::SInt8))
+  -- Solution #1:
+  --   s0 = -128 :: Int8
+  --   s1 =   -1 :: Int8
+  -- This is the only solution.
+
+  bvDivO :: a -> a -> (SBool, SBool)
+
+  -- | Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is
+  -- @minBound@:
+  --
+  -- >>> prove $ \x -> x .== minBound <=> snd (bvNegO (x::SInt16))
+  -- Q.E.D.
+  bvNegO :: a -> (SBool, SBool)
+
+instance ArithOverflow SWord8  where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+instance ArithOverflow SWord16 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+instance ArithOverflow SWord32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+instance ArithOverflow SWord64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+instance ArithOverflow SInt8   where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+instance ArithOverflow SInt16  where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+instance ArithOverflow SInt32  where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+instance ArithOverflow SInt64  where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}
+
+instance ArithOverflow SVal where
+  bvAddO     = signPick2 bvuaddo     bvsaddo
+  bvSubO     = signPick2 bvusubo     bvssubo
+  bvMulO     = signPick2 bvumulo     bvsmulo
+  bvMulOFast = signPick2 bvumuloFast bvsmuloFast
+  bvDivO     = signPick2 bvudivo     bvsdivo
+  bvNegO     = signPick1 bvunego     bvsnego
+
+-- | Zero-extend to given bits
+zx :: Int -> SVal -> SVal
+zx n a
+ | n < sa = error $ "Data.SBV: Unexpected zero extension: from: " ++ show (intSizeOf a) ++ " to: " ++ show n
+ | True   = p `svJoin` a
+ where sa = intSizeOf a
+       s  = hasSign a
+       p  = svInteger (KBounded s (n - sa)) 0
+
+-- | Sign-extend to given bits. Note that we keep the signedness of the argument.
+sx :: Int -> SVal -> SVal
+sx n a
+ | n < sa = error $ "Data.SBV: Unexpected sign extension: from: " ++ show (intSizeOf a) ++ " to: " ++ show n
+ | True   = p `svJoin` a
+ where sa = intSizeOf a
+       mk = svInteger $ KBounded (hasSign a) (n - sa)
+       p  = svIte (pos a) (mk 0) (mk (-1))
+
+-- | Get the sign-bit
+signBit :: SVal -> SVal
+signBit x = x `svTestBit` (intSizeOf x - 1)
+
+-- | Is the sign-bit high?
+neg :: SVal -> SVal
+neg x = signBit x `svEqual` svTrue
+
+-- | Is the sign-bit low?
+pos :: SVal -> SVal
+pos x = signBit x `svEqual` svFalse
+
+-- | Do these have the same sign?
+sameSign :: SVal -> SVal -> SVal
+sameSign x y = (pos x `svAnd` pos y) `svOr` (neg x `svAnd` neg y)
+
+-- | Do these have opposing signs?
+diffSign :: SVal -> SVal -> SVal
+diffSign x y = svNot (sameSign x y)
+
+-- | Check all true
+svAll :: [SVal] -> SVal
+svAll = foldr svAnd svTrue
+
+-- | Are all the bits between a b (inclusive) zero?
+allZero :: Int -> Int -> SBV a -> SVal
+allZero m n (SBV x)
+  | m >= sz || n < 0 || m < n
+  = error $ "Data.SBV.Tools.Overflow.allZero: Received unexpected parameters: " ++ show (m, n, sz)
+  | True
+  = svAll [svTestBit x i `svEqual` svFalse | i <- [m, m-1 .. n]]
+  where sz = intSizeOf x
+
+-- | Are all the bits between a b (inclusive) one?
+allOne :: Int -> Int -> SBV a -> SVal
+allOne m n (SBV x)
+  | m >= sz || n < 0 || m < n
+  = error $ "Data.SBV.Tools.Overflow.allOne: Received unexpected parameters: " ++ show (m, n, sz)
+  | True
+  = svAll [svTestBit x i `svEqual` svTrue | i <- [m, m-1 .. n]]
+  where sz = intSizeOf x
+
+-- | Unsigned addition. Can only overflow.
+bvuaddo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvuaddo n x y = (underflow, overflow)
+  where underflow = svFalse
+
+        n'       = n+1
+        overflow = neg $ zx n' x `svPlus` zx n' y
+
+-- | Signed addition.
+bvsaddo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvsaddo _n x y = (underflow, overflow)
+  where underflow = svAll [neg x, neg y, pos (x `svPlus` y)]
+        overflow  = svAll [pos x, pos y, neg (x `svPlus` y)]
+
+-- | Unsigned subtraction. Can only underflow.
+bvusubo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvusubo _n x y = (underflow, overflow)
+  where underflow = y `svGreaterThan` x
+        overflow  = svFalse
+
+-- | Signed subtraction.
+bvssubo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvssubo _n x y = (underflow, overflow)
+  where underflow = svAll [neg x, pos y, pos (x `svMinus` y)]
+        overflow  = svAll [pos x, neg y, neg (x `svMinus` y)]
+
+-- | Unsigned multiplication. Can only overflow.
+bvumulo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvumulo 0 _ _ = (svFalse,   svFalse)
+bvumulo n x y = (underflow, overflow)
+  where underflow = svFalse
+
+        n1        = n+1
+        overflow1 = signBit $ zx n1 x `svTimes` zx n1 y
+
+        -- From Z3 sources:
+        --
+        -- expr_ref ovf(m()), v(m()), tmp(m());
+        -- ovf = m().mk_false();
+        -- v = m().mk_false();
+        -- for (unsigned i = 1; i < sz; ++i) {
+        --    mk_or(ovf, a_bits[sz-i], ovf);
+        --    mk_and(ovf, b_bits[i], tmp);
+        --    mk_or(tmp, v, v);
+        -- }
+        -- overflow2 = v;
+        --
+        overflow2 = go 1 svFalse svFalse
+          where go i ovf v
+                 | i >= n = v
+                 | True   = go (i+1) ovf' v'
+                 where ovf' = ovf  `svOr`  (x `svTestBit` (n-i))
+                       tmp  = ovf' `svAnd` (y `svTestBit` i)
+                       v'   = tmp `svOr` v
+
+        overflow = overflow1 `svOr` overflow2
+
+-- | Signed multiplication.
+bvsmulo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvsmulo 0 _ _ = (svFalse,   svFalse)
+bvsmulo n x y = (underflow, overflow)
+  where underflow = diffSign x y `svAnd` overflowPossible
+        overflow  = sameSign x y `svAnd` overflowPossible
+
+        n1        = n+1
+        overflow1 = (xy1 `svTestBit` n) `svXOr` (xy1 `svTestBit` (n-1))
+           where xy1 = sx n1 x `svTimes` sx n1 y
+
+        -- From Z3 sources:
+        -- expr_ref v(m()), tmp(m()), a(m()), b(m()), a_acc(m()), sign(m());
+        -- a_acc = m().mk_false();
+        -- v = m().mk_false();
+        -- for (unsigned i = 1; i + 1 < sz; ++i) {
+        --    mk_xor(b_bits[sz-1], b_bits[i], b);
+        --    mk_xor(a_bits[sz-1], a_bits[sz-1-i], a);
+        --    mk_or(a, a_acc, a_acc);
+        --    mk_and(a_acc, b, tmp);
+        --    mk_or(tmp, v, v);
+        -- }
+        -- overflow2 = v;
+        overflow2 = go 1 svFalse svFalse
+           where sY = signBit y
+                 sX = signBit x
+                 go i v a_acc
+                  | i + 1 >= n = v
+                  | True       = go (i+1) v' a_acc'
+                  where b      = sY `svXOr` (y `svTestBit` i)
+                        a      = sX `svXOr` (x `svTestBit` (n-1-i))
+                        a_acc' = a `svOr` a_acc
+                        tmp    = a_acc' `svAnd` b
+                        v'     = tmp `svOr` v
+
+        overflowPossible = overflow1 `svOr` overflow2
+
+-- | Is this a concrete value?
+known :: SVal -> Bool
+known (SVal _ (Left _)) = True
+known _                 = False
+
+-- | Unsigned multiplication, fast version using z3 primitives.
+bvumuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
+bvumuloFast n x y
+   | known x && known y                         -- Not particularly fast, but avoids shipping of to the solver
+   = bvumulo n x y
+   | True
+   = (underflow, overflow)
+  where underflow = fst $ bvumulo n x y         -- No internal version for underflow exists (because it can't underflow)
+        overflow  = svMkOverflow Overflow_UMul_OVFL x y
+
+-- | Signed multiplication, fast version using z3 primitives.
+bvsmuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
+bvsmuloFast n x y
+  | known x && known y                -- Not particularly fast, but avoids shipping of to the solver
+  = bvsmulo n x y
+  | True
+  = (underflow, overflow)
+  where underflow = svMkOverflow Overflow_SMul_UDFL x y
+        overflow  = svMkOverflow Overflow_SMul_OVFL x y
+
+-- | Unsigned division. Neither underflows, nor overflows.
+bvudivo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvudivo _ _ _ = (underflow, overflow)
+  where underflow = svFalse
+        overflow  = svFalse
+
+-- | Signed division. Can only overflow.
+bvsdivo :: Int -> SVal -> SVal -> (SVal, SVal)
+bvsdivo n x y = (underflow, overflow)
+  where underflow = svFalse
+
+        ones      = svInteger (KBounded True n) (-1)
+        topSet    = svInteger (KBounded True n) (2^(n-1))
+
+        overflow = svAll [x `svEqual` topSet, y `svEqual` ones]
+
+-- | Unsigned negation. Neither underflows, nor overflows.
+bvunego :: Int -> SVal -> (SVal, SVal)
+bvunego _ _ = (underflow, overflow)
+  where underflow = svFalse
+        overflow  = svFalse
+
+-- | Signed negation. Can only overflow.
+bvsnego :: Int -> SVal -> (SVal, SVal)
+bvsnego n x = (underflow, overflow)
+  where underflow = svFalse
+
+        topSet    = svInteger (KBounded True n) (2^(n-1))
+        overflow  = x `svEqual` topSet
+
+-- | Detecting underflow/overflow conditions for casting between bit-vectors. The first output is the result,
+-- the second component itself is a pair with the first boolean indicating underflow and the second indicating overflow.
+--
+-- >>> sFromIntegralO (256 :: SInt16) :: (SWord8, (SBool, SBool))
+-- (0 :: SWord8,(False,True))
+-- >>> sFromIntegralO (-2 :: SInt16) :: (SWord8, (SBool, SBool))
+-- (254 :: SWord8,(True,False))
+-- >>> sFromIntegralO (2 :: SInt16) :: (SWord8, (SBool, SBool))
+-- (2 :: SWord8,(False,False))
+-- >>> prove $ \x -> sFromIntegralO (x::SInt32) .== (sFromIntegral x :: SInteger, (false, false))
+-- Q.E.D.
+--
+-- As the last example shows, converting to `sInteger` never underflows or overflows for any value.
+sFromIntegralO :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> (SBV b, (SBool, SBool))
+sFromIntegralO x = case (kindOf x, kindOf (undefined :: b)) of
+                     (KBounded False n, KBounded False m) -> (res, u2u n m)
+                     (KBounded False n, KBounded True  m) -> (res, u2s n m)
+                     (KBounded True n,  KBounded False m) -> (res, s2u n m)
+                     (KBounded True n,  KBounded True  m) -> (res, s2s n m)
+                     (KUnbounded,       KBounded s m)     -> (res, checkBounds s m)
+                     (KBounded{},       KUnbounded)       -> (res, (false, false))
+                     (KUnbounded,       KUnbounded)       -> (res, (false, false))
+                     (kFrom,            kTo)              -> error $ "sFromIntegralO: Expected bounded-BV types, received: " ++ show (kFrom, kTo)
+
+  where res :: SBV b
+        res = sFromIntegral x
+
+        checkBounds :: Bool -> Int -> (SBool, SBool)
+        checkBounds signed sz = (ix .< literal lb, ix .> literal ub)
+          where ix :: SInteger
+                ix = sFromIntegral x
+
+                s :: Integer
+                s = fromIntegral sz
+
+                ub :: Integer
+                ub | signed = 2^(s - 1) - 1
+                   | True   = 2^s       - 1
+
+                lb :: Integer
+                lb | signed = -ub-1
+                   | True   = 0
+
+        u2u :: Int -> Int -> (SBool, SBool)
+        u2u n m = (underflow, overflow)
+          where underflow  = false
+                overflow
+                  | n <= m = false
+                  | True   = SBV $ svNot $ allZero (n-1) m x
+
+        u2s :: Int -> Int -> (SBool, SBool)
+        u2s n m = (underflow, overflow)
+          where underflow = false
+                overflow
+                  | m > n = false
+                  | True  = SBV $ svNot $ allZero (n-1) (m-1) x
+
+        s2u :: Int -> Int -> (SBool, SBool)
+        s2u n m = (underflow, overflow)
+          where underflow = SBV $ (unSBV x `svTestBit` (n-1)) `svEqual` svTrue
+
+                overflow
+                  | m >= n - 1 = false
+                  | True       = SBV $ svAll [(unSBV x `svTestBit` (n-1)) `svEqual` svFalse, svNot $ allZero (n-1) m x]
+
+        s2s :: Int -> Int -> (SBool, SBool)
+        s2s n m = (underflow, overflow)
+          where underflow
+                  | m > n = false
+                  | True  = SBV $ svAll [(unSBV x `svTestBit` (n-1)) `svEqual` svTrue,  svNot $ allOne  (n-1) (m-1) x]
+
+                overflow
+                  | m > n = false
+                  | True  = SBV $ svAll [(unSBV x `svTestBit` (n-1)) `svEqual` svFalse, svNot $ allZero (n-1) (m-1) x]
+
+-- Helpers
+l2 :: (SVal -> SVal -> (SBool, SBool)) -> SBV a -> SBV a -> (SBool, SBool)
+l2 f (SBV a) (SBV b) = f a b
+
+l1 :: (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
+l1 f (SBV a) = f a
+
+signPick2 :: (Int -> SVal -> SVal -> (SVal, SVal)) -> (Int -> SVal -> SVal -> (SVal, SVal)) -> (SVal -> SVal -> (SBool, SBool))
+signPick2 fu fs a b
+ | hasSign a = let (u, o) = fs n a b in (SBV u, SBV o)
+ | True      = let (u, o) = fu n a b in (SBV u, SBV o)
+ where n = intSizeOf a
+
+signPick1 :: (Int -> SVal -> (SVal, SVal)) -> (Int -> SVal -> (SVal, SVal)) -> (SVal -> (SBool, SBool))
+signPick1 fu fs a
+ | hasSign a = let (u, o) = fs n a in (SBV u, SBV o)
+ | True      = let (u, o) = fu n a in (SBV u, SBV o)
+ where n = intSizeOf a
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
@@ -102,6 +102,20 @@
   | isNegativeZero b = isNegativeZero a
   | True             = a == b
 
+-- | Ordering for floats, avoiding the +0/-0/NaN issues. Note that this is
+-- essentially used for indexing into a map, so we need to be total. Thus,
+-- the order we pick is:
+--    NaN -oo -0 +0 +oo
+-- The placement of NaN here is questionable, but immaterial.
+fpCompareObjectH :: RealFloat a => a -> a -> Ordering
+fpCompareObjectH a b
+  | a `fpIsEqualObjectH` b   = EQ
+  | isNaN a                  = LT
+  | isNaN b                  = GT
+  | isNegativeZero a, b == 0 = LT
+  | isNegativeZero b, a == 0 = GT
+  | True                     = a `compare` b
+
 -- | Check if a number is "normal." Note that +0/-0 is not considered a normal-number
 -- and also this is not simply the negation of isDenormalized!
 fpIsNormalizedH :: RealFloat a => a -> Bool
diff --git a/Documentation/SBV/Examples/Existentials/Diophantine.hs b/Documentation/SBV/Examples/Existentials/Diophantine.hs
--- a/Documentation/SBV/Examples/Existentials/Diophantine.hs
+++ b/Documentation/SBV/Examples/Existentials/Diophantine.hs
@@ -12,7 +12,6 @@
 module Documentation.SBV.Examples.Existentials.Diophantine where
 
 import Data.SBV
-import Data.SBV.Control
 
 --------------------------------------------------------------------------------------------------
 -- * Representing solutions
diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs
--- a/Documentation/SBV/Examples/Misc/Floating.hs
+++ b/Documentation/SBV/Examples/Misc/Floating.hs
@@ -56,16 +56,16 @@
 --
 -- >>> assocPlusRegular
 -- Falsifiable. Counter-example:
---   x =  1.9259302e-34 :: Float
---   y = -1.9259117e-34 :: Float
---   z =  -1.814176e-39 :: Float
+--   x =  -1.844675e19 :: Float
+--   y =  8.7960925e12 :: Float
+--   z = -2.4178333e24 :: Float
 --
 -- Indeed, we have:
 --
--- >>> ((1.9259302e-34) + ((-1.9259117e-34) + (-1.814176e-39))) :: Float
--- 3.4438e-41
--- >>> (((1.9259302e-34) + ((-1.9259117e-34))) + (-1.814176e-39)) :: Float
--- 3.4014e-41
+-- >>> (-1.844675e19) + ((8.7960925e12)  + (-2.4178333e24)):: Float
+-- -2.417852e24
+-- >>> ((-1.844675e19) + (8.7960925e12))  + (-2.4178333e24) :: Float
+-- -2.4178516e24
 --
 -- Note the difference between two additions!
 assocPlusRegular :: IO ThmResult
@@ -87,17 +87,17 @@
 --
 -- >>> nonZeroAddition
 -- Falsifiable. Counter-example:
---   a = 2.424457e-38 :: Float
---   b =     -1.0e-45 :: Float
+--   a = -2.524355e-29 :: Float
+--   b =  9.403955e-38 :: Float
 --
 -- Indeed, we have:
 --
--- >>> (2.424457e-38 + (-1.0e-45)) == (2.424457e-38 :: Float)
+-- >>> (-2.524355e-29 + 9.403955e-38) == (-2.524355e-29 :: Float)
 -- True
 --
 -- But:
 --
--- >>> -1.0e-45 == (0 :: Float)
+-- >>> 9.403955e-38 == (0 :: Float)
 -- False
 --
 nonZeroAddition :: IO ThmResult
@@ -118,13 +118,13 @@
 --
 -- >>> multInverse
 -- Falsifiable. Counter-example:
---   a = 1.119056263978578e-308 :: Double
+--   a = 8.988465678497178e307 :: Double
 --
 -- Indeed, we have:
 --
--- >>> let a = 1.119056263978578e-308 :: Double
+-- >>> let a = 8.988465678497178e307 :: Double
 -- >>> a * (1/a)
--- 0.9999999999999999
+-- 1.0000000000000002
 multInverse :: IO ThmResult
 multInverse = prove $ do a <- sDouble "a"
                          constrain $ fpIsPoint a
diff --git a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs
--- a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs
+++ b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs
@@ -59,7 +59,7 @@
 -- | Give symbolic colors a name for convenience.
 type SColor = SBV Color
 
--- | Use 8-bit words for button numners, even though we only have 1 to 19.
+-- | Use 8-bit words for button numbers, even though we only have 1 to 19.
 type Button  = Word8
 
 -- | Symbolic version of button.
diff --git a/Documentation/SBV/Examples/Queries/Interpolants.hs b/Documentation/SBV/Examples/Queries/Interpolants.hs
--- a/Documentation/SBV/Examples/Queries/Interpolants.hs
+++ b/Documentation/SBV/Examples/Queries/Interpolants.hs
@@ -7,6 +7,9 @@
 -- Stability   :  experimental
 --
 -- Demonstrates extraction of interpolants via queries.
+--
+-- N.B. As of Z3 version 4.8.0; Z3 no longer supports interpolants. You need
+-- to use the MathSAT backend for this example to work.
 -----------------------------------------------------------------------------
 
 module Documentation.SBV.Examples.Queries.Interpolants where
@@ -14,37 +17,45 @@
 import Data.SBV
 import Data.SBV.Control
 
--- | Compute the interpolant for formulas @y = 2x@ and @y = 2z+1@.
--- These formulas are not satisfiable together since it would mean
--- @y@ is both even and odd at the same time. An interpolant for
--- this pair of formulas is a formula that's expressed only in terms
--- of @y@, which is the only common symbol among them. We have:
+-- | Compute the interpolant for the following sets of formulas:
 --
--- >>> runSMT evenOdd
--- ["(<= 0 (+ (div s1 2) (div (* (- 1) s1) 2)))"]
+--     @{x - 3y >= -1, x + y >= 0}@
 --
--- This is a bit hard to read unfortunately, due to translation artifacts and use of strings. To analyze,
--- we need to know that @s1@ is @y@ through SBV's translation. Let's express it in
--- regular infix notation with @y@ for @s1@:
+-- AND
 --
--- @ 0 <= (y `div` 2) + ((-y) `div` 2)@
+--     @{z - 2x >= 3, 2z <= 1}@
 --
--- Notice that the only symbol is @y@, as required. To establish that this is
--- indeed an interpolant, we should establish that when @y@ is even, this formula
--- is @True@; and if @y@ is odd, then then it should be @False@. You can argue
--- mathematically that this indeed the case, but let's just use SBV to prove these:
+-- where the variables are integers.  Note that these sets of
+-- formulas are themselves satisfiable, but not taken all together.
+-- The pair @(x, y) = (0, 0)@ satisfies the first set. The pair @(x, z) = (-2, 0)@
+-- satisfies the second. However, there's no triple @(x, y, z)@ that satisfies all
+-- these four formulas together. We can use SBV to check this fact:
 --
--- >>> prove $ \y -> (y `sMod` 2 .== 0) ==> (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))
+-- >>> sat $ \x y z -> bAnd [x - 3*y .>= -1, x + y .>= 0, z - 2*x .>= 3, 2 * z .<= (1::SInteger)]
+-- Unsatisfiable
+--
+-- An interpolant for these sets would only talk about the variable @x@ that is common
+-- to both. We have:
+--
+-- >>> runSMTWith mathSAT example
+-- "(<= 0 s0)"
+--
+-- Notice that we get a string back, not a term; so there's some back-translation we need to do. We
+-- know that @s0@ is @x@ through our translation mechanism, so the interpolant is saying that @x >= 0@
+-- is entailed by the first set of formulas, and is inconsistent with the second. Let's use SBV
+-- to indeed show that this is the case:
+--
+-- >>> prove $ \x y -> (x - 3*y .>= -1 &&& x + y .>= 0) ==> (x .>= (0::SInteger))
 -- Q.E.D.
 --
 -- And:
 --
--- >>> prove $ \y -> (y `sMod` 2 .== 1) ==> bnot (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))
+-- >>> prove $ \x z -> (z - 2*x .>= 3 &&& 2 * z .<= 1) ==> bnot (x .>= (0::SInteger))
 -- Q.E.D.
 --
 -- This establishes that we indeed have an interpolant!
-evenOdd :: Symbolic [String]
-evenOdd = do
+example :: Symbolic String
+example = do
        x <- sInteger "x"
        y <- sInteger "y"
        z <- sInteger "z"
@@ -52,14 +63,16 @@
        -- tell the solver we want interpolants
        setOption $ ProduceInterpolants True
 
-       -- create named constraints, which will allow
-       -- computation of the interpolants for our formulas
-       namedConstraint "y is even" $ y .== 2*x
-       namedConstraint "y is odd"  $ y .== 2*z + 1
+       -- create interpolation constraints. MathSAT requires the relevant formulas
+       -- to be marked with the attribute :interpolation-group
+       constrainWithAttribute [(":interpolation-group", "A")] $ x - 3*y .>= -1
+       constrainWithAttribute [(":interpolation-group", "A")] $ x + y   .>=  0
+       constrainWithAttribute [(":interpolation-group", "B")] $ z - 2*x .>=  3
+       constrainWithAttribute [(":interpolation-group", "B")] $ 2*z     .<=  1
 
        -- To obtain the interpolant, we run a query
        query $ do cs <- checkSat
                   case cs of
-                    Unsat -> getInterpolant ["y is even", "y is odd"]
+                    Unsat -> getInterpolant ["A"]
                     Sat   -> error "Unexpected sat result!"
                     Unk   -> error "Unexpected unknown result!"
diff --git a/SBVTestSuite/GoldFiles/floats_cgen.gold b/SBVTestSuite/GoldFiles/floats_cgen.gold
--- a/SBVTestSuite/GoldFiles/floats_cgen.gold
+++ b/SBVTestSuite/GoldFiles/floats_cgen.gold
@@ -2574,6 +2574,7 @@
 
 CC?=gcc
 CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+LDFLAGS?=-lm
 AR?=ar
 ARFLAGS?=cr
 
@@ -2583,7 +2584,7 @@
 	${AR} ${ARFLAGS} $@ $^
 
 floatCodeGen_driver: floatCodeGen_driver.c floatCodeGen.h
-	${CC} ${CCFLAGS} $< -o $@ floatCodeGen.a
+	${CC} ${CCFLAGS} $< -o $@ floatCodeGen.a ${LDFLAGS}
 
 toFP_Int8_ToFloat.o: toFP_Int8_ToFloat.c floatCodeGen.h
 	${CC} ${CCFLAGS} -c $< -o $@
diff --git a/SBVTestSuite/GoldFiles/pareto1.gold b/SBVTestSuite/GoldFiles/pareto1.gold
--- a/SBVTestSuite/GoldFiles/pareto1.gold
+++ b/SBVTestSuite/GoldFiles/pareto1.gold
@@ -5,89 +5,89 @@
   max_x_plus_y = 0 :: Integer
   min_y        = 0 :: Integer
 Pareto front #2: Optimal model:
-  x            = 0 :: Integer
-  y            = 1 :: Integer
-  min_x        = 0 :: Integer
-  max_x_plus_y = 1 :: Integer
-  min_y        = 1 :: Integer
-Pareto front #3: Optimal model:
-  x            = 4 :: Integer
+  x            = 1 :: Integer
   y            = 0 :: Integer
-  min_x        = 4 :: Integer
-  max_x_plus_y = 4 :: Integer
+  min_x        = 1 :: Integer
+  max_x_plus_y = 1 :: Integer
   min_y        = 0 :: Integer
-Pareto front #4: Optimal model:
-  x            = 4 :: Integer
-  y            = 4 :: Integer
-  min_x        = 4 :: Integer
-  max_x_plus_y = 8 :: Integer
-  min_y        = 4 :: Integer
-Pareto front #5: Optimal model:
+Pareto front #3: Optimal model:
   x            = 0 :: Integer
   y            = 2 :: Integer
   min_x        = 0 :: Integer
   max_x_plus_y = 2 :: Integer
   min_y        = 2 :: Integer
-Pareto front #6: Optimal model:
-  x            = 2 :: Integer
-  y            = 2 :: Integer
-  min_x        = 2 :: Integer
-  max_x_plus_y = 4 :: Integer
-  min_y        = 2 :: Integer
-Pareto front #7: Optimal model:
+Pareto front #4: Optimal model:
   x            = 1 :: Integer
-  y            = 0 :: Integer
+  y            = 1 :: Integer
   min_x        = 1 :: Integer
+  max_x_plus_y = 2 :: Integer
+  min_y        = 1 :: Integer
+Pareto front #5: Optimal model:
+  x            = 0 :: Integer
+  y            = 1 :: Integer
+  min_x        = 0 :: Integer
   max_x_plus_y = 1 :: Integer
-  min_y        = 0 :: Integer
-Pareto front #8: Optimal model:
-  x            = 5 :: Integer
-  y            = 0 :: Integer
-  min_x        = 5 :: Integer
-  max_x_plus_y = 5 :: Integer
-  min_y        = 0 :: Integer
-Pareto front #9: Optimal model:
-  x            = 5 :: Integer
-  y            = 2 :: Integer
-  min_x        = 5 :: Integer
-  max_x_plus_y = 7 :: Integer
-  min_y        = 2 :: Integer
-Pareto front #10: Optimal model:
+  min_y        = 1 :: Integer
+Pareto front #6: Optimal model:
   x            = 1 :: Integer
   y            = 2 :: Integer
   min_x        = 1 :: Integer
   max_x_plus_y = 3 :: Integer
   min_y        = 2 :: Integer
-Pareto front #11: Optimal model:
-  x            = 4 :: Integer
-  y            = 2 :: Integer
-  min_x        = 4 :: Integer
-  max_x_plus_y = 6 :: Integer
-  min_y        = 2 :: Integer
-Pareto front #12: Optimal model:
+Pareto front #7: Optimal model:
   x            = 2 :: Integer
   y            = 0 :: Integer
   min_x        = 2 :: Integer
   max_x_plus_y = 2 :: Integer
   min_y        = 0 :: Integer
-Pareto front #13: Optimal model:
+Pareto front #8: Optimal model:
+  x            = 2 :: Integer
+  y            = 1 :: Integer
+  min_x        = 2 :: Integer
+  max_x_plus_y = 3 :: Integer
+  min_y        = 1 :: Integer
+Pareto front #9: Optimal model:
   x            = 3 :: Integer
   y            = 0 :: Integer
   min_x        = 3 :: Integer
   max_x_plus_y = 3 :: Integer
   min_y        = 0 :: Integer
-Pareto front #14: Optimal model:
+Pareto front #10: Optimal model:
   x            = 3 :: Integer
-  y            = 2 :: Integer
+  y            = 1 :: Integer
   min_x        = 3 :: Integer
+  max_x_plus_y = 4 :: Integer
+  min_y        = 1 :: Integer
+Pareto front #11: Optimal model:
+  x            = 4 :: Integer
+  y            = 0 :: Integer
+  min_x        = 4 :: Integer
+  max_x_plus_y = 4 :: Integer
+  min_y        = 0 :: Integer
+Pareto front #12: Optimal model:
+  x            = 4 :: Integer
+  y            = 1 :: Integer
+  min_x        = 4 :: Integer
   max_x_plus_y = 5 :: Integer
-  min_y        = 2 :: Integer
-Pareto front #15: Optimal model:
-  x            = 1 :: Integer
+  min_y        = 1 :: Integer
+Pareto front #13: Optimal model:
+  x            = 5 :: Integer
+  y            = 0 :: Integer
+  min_x        = 5 :: Integer
+  max_x_plus_y = 5 :: Integer
+  min_y        = 0 :: Integer
+Pareto front #14: Optimal model:
+  x            = 5 :: Integer
   y            = 1 :: Integer
-  min_x        = 1 :: Integer
-  max_x_plus_y = 2 :: Integer
+  min_x        = 5 :: Integer
+  max_x_plus_y = 6 :: Integer
   min_y        = 1 :: Integer
+Pareto front #15: Optimal model:
+  x            = 2 :: Integer
+  y            = 2 :: Integer
+  min_x        = 2 :: Integer
+  max_x_plus_y = 4 :: Integer
+  min_y        = 2 :: Integer
 Pareto front #16: Optimal model:
   x            = 0 :: Integer
   y            = 3 :: Integer
@@ -113,68 +113,68 @@
   max_x_plus_y = 5 :: Integer
   min_y        = 4 :: Integer
 Pareto front #20: Optimal model:
-  x            = 4 :: Integer
-  y            = 1 :: Integer
-  min_x        = 4 :: Integer
+  x            = 2 :: Integer
+  y            = 3 :: Integer
+  min_x        = 2 :: Integer
   max_x_plus_y = 5 :: Integer
-  min_y        = 1 :: Integer
+  min_y        = 3 :: Integer
 Pareto front #21: Optimal model:
-  x            = 5 :: Integer
-  y            = 1 :: Integer
-  min_x        = 5 :: Integer
+  x            = 2 :: Integer
+  y            = 4 :: Integer
+  min_x        = 2 :: Integer
   max_x_plus_y = 6 :: Integer
-  min_y        = 1 :: Integer
+  min_y        = 4 :: Integer
 Pareto front #22: Optimal model:
-  x            = 4 :: Integer
-  y            = 3 :: Integer
-  min_x        = 4 :: Integer
-  max_x_plus_y = 7 :: Integer
-  min_y        = 3 :: Integer
+  x            = 3 :: Integer
+  y            = 2 :: Integer
+  min_x        = 3 :: Integer
+  max_x_plus_y = 5 :: Integer
+  min_y        = 2 :: Integer
 Pareto front #23: Optimal model:
-  x            = 5 :: Integer
+  x            = 3 :: Integer
   y            = 3 :: Integer
-  min_x        = 5 :: Integer
-  max_x_plus_y = 8 :: Integer
+  min_x        = 3 :: Integer
+  max_x_plus_y = 6 :: Integer
   min_y        = 3 :: Integer
 Pareto front #24: Optimal model:
-  x            = 5 :: Integer
+  x            = 3 :: Integer
   y            = 4 :: Integer
-  min_x        = 5 :: Integer
-  max_x_plus_y = 9 :: Integer
+  min_x        = 3 :: Integer
+  max_x_plus_y = 7 :: Integer
   min_y        = 4 :: Integer
 Pareto front #25: Optimal model:
-  x            = 2 :: Integer
-  y            = 1 :: Integer
-  min_x        = 2 :: Integer
-  max_x_plus_y = 3 :: Integer
-  min_y        = 1 :: Integer
+  x            = 4 :: Integer
+  y            = 2 :: Integer
+  min_x        = 4 :: Integer
+  max_x_plus_y = 6 :: Integer
+  min_y        = 2 :: Integer
 Pareto front #26: Optimal model:
-  x            = 3 :: Integer
-  y            = 1 :: Integer
-  min_x        = 3 :: Integer
-  max_x_plus_y = 4 :: Integer
-  min_y        = 1 :: Integer
+  x            = 5 :: Integer
+  y            = 2 :: Integer
+  min_x        = 5 :: Integer
+  max_x_plus_y = 7 :: Integer
+  min_y        = 2 :: Integer
 Pareto front #27: Optimal model:
-  x            = 2 :: Integer
+  x            = 4 :: Integer
   y            = 3 :: Integer
-  min_x        = 2 :: Integer
-  max_x_plus_y = 5 :: Integer
+  min_x        = 4 :: Integer
+  max_x_plus_y = 7 :: Integer
   min_y        = 3 :: Integer
 Pareto front #28: Optimal model:
-  x            = 3 :: Integer
+  x            = 5 :: Integer
   y            = 3 :: Integer
-  min_x        = 3 :: Integer
-  max_x_plus_y = 6 :: Integer
+  min_x        = 5 :: Integer
+  max_x_plus_y = 8 :: Integer
   min_y        = 3 :: Integer
 Pareto front #29: Optimal model:
-  x            = 2 :: Integer
+  x            = 4 :: Integer
   y            = 4 :: Integer
-  min_x        = 2 :: Integer
-  max_x_plus_y = 6 :: Integer
+  min_x        = 4 :: Integer
+  max_x_plus_y = 8 :: Integer
   min_y        = 4 :: Integer
 Pareto front #30: Optimal model:
-  x            = 3 :: Integer
+  x            = 5 :: Integer
   y            = 4 :: Integer
-  min_x        = 3 :: Integer
-  max_x_plus_y = 7 :: Integer
+  min_x        = 5 :: Integer
+  max_x_plus_y = 9 :: Integer
   min_y        = 4 :: Integer
diff --git a/SBVTestSuite/GoldFiles/pareto2.gold b/SBVTestSuite/GoldFiles/pareto2.gold
--- a/SBVTestSuite/GoldFiles/pareto2.gold
+++ b/SBVTestSuite/GoldFiles/pareto2.gold
@@ -1,182 +1,182 @@
 Pareto front #1: Optimal model:
-  x            = 0 :: Integer
-  y            = 4 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 4 :: Integer
-  max_x_plus_y = 4 :: Integer
+  x            =  0 :: Integer
+  y            = -1 :: Integer
+  min_x        =  0 :: Integer
+  max_y        = -1 :: Integer
+  max_x_plus_y = -1 :: Integer
 Pareto front #2: Optimal model:
-  x            = 0 :: Integer
-  y            = 5 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 5 :: Integer
-  max_x_plus_y = 5 :: Integer
+  x            =  0 :: Integer
+  y            = -2 :: Integer
+  min_x        =  0 :: Integer
+  max_y        = -2 :: Integer
+  max_x_plus_y = -2 :: Integer
 Pareto front #3: Optimal model:
-  x            = 0 :: Integer
-  y            = 6 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 6 :: Integer
-  max_x_plus_y = 6 :: Integer
+  x            =  0 :: Integer
+  y            = -3 :: Integer
+  min_x        =  0 :: Integer
+  max_y        = -3 :: Integer
+  max_x_plus_y = -3 :: Integer
 Pareto front #4: Optimal model:
-  x            = 0 :: Integer
-  y            = 7 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 7 :: Integer
-  max_x_plus_y = 7 :: Integer
+  x            =  0 :: Integer
+  y            = -4 :: Integer
+  min_x        =  0 :: Integer
+  max_y        = -4 :: Integer
+  max_x_plus_y = -4 :: Integer
 Pareto front #5: Optimal model:
-  x            = 0 :: Integer
-  y            = 8 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 8 :: Integer
-  max_x_plus_y = 8 :: Integer
+  x            =  0 :: Integer
+  y            = -5 :: Integer
+  min_x        =  0 :: Integer
+  max_y        = -5 :: Integer
+  max_x_plus_y = -5 :: Integer
 Pareto front #6: Optimal model:
-  x            = 0 :: Integer
-  y            = 9 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 9 :: Integer
-  max_x_plus_y = 9 :: Integer
+  x            =  0 :: Integer
+  y            = -6 :: Integer
+  min_x        =  0 :: Integer
+  max_y        = -6 :: Integer
+  max_x_plus_y = -6 :: Integer
 Pareto front #7: Optimal model:
   x            =  0 :: Integer
-  y            = 10 :: Integer
+  y            = -7 :: Integer
   min_x        =  0 :: Integer
-  max_y        = 10 :: Integer
-  max_x_plus_y = 10 :: Integer
+  max_y        = -7 :: Integer
+  max_x_plus_y = -7 :: Integer
 Pareto front #8: Optimal model:
   x            =  0 :: Integer
-  y            = 11 :: Integer
+  y            = -8 :: Integer
   min_x        =  0 :: Integer
-  max_y        = 11 :: Integer
-  max_x_plus_y = 11 :: Integer
+  max_y        = -8 :: Integer
+  max_x_plus_y = -8 :: Integer
 Pareto front #9: Optimal model:
   x            =  0 :: Integer
-  y            = 12 :: Integer
+  y            = -9 :: Integer
   min_x        =  0 :: Integer
-  max_y        = 12 :: Integer
-  max_x_plus_y = 12 :: Integer
+  max_y        = -9 :: Integer
+  max_x_plus_y = -9 :: Integer
 Pareto front #10: Optimal model:
-  x            =  0 :: Integer
-  y            = 13 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 13 :: Integer
-  max_x_plus_y = 13 :: Integer
+  x            =   0 :: Integer
+  y            = -10 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -10 :: Integer
+  max_x_plus_y = -10 :: Integer
 Pareto front #11: Optimal model:
-  x            =  0 :: Integer
-  y            = 14 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 14 :: Integer
-  max_x_plus_y = 14 :: Integer
+  x            =   0 :: Integer
+  y            = -11 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -11 :: Integer
+  max_x_plus_y = -11 :: Integer
 Pareto front #12: Optimal model:
-  x            =  0 :: Integer
-  y            = 15 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 15 :: Integer
-  max_x_plus_y = 15 :: Integer
+  x            =   0 :: Integer
+  y            = -12 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -12 :: Integer
+  max_x_plus_y = -12 :: Integer
 Pareto front #13: Optimal model:
-  x            =  0 :: Integer
-  y            = 16 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 16 :: Integer
-  max_x_plus_y = 16 :: Integer
+  x            =   0 :: Integer
+  y            = -13 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -13 :: Integer
+  max_x_plus_y = -13 :: Integer
 Pareto front #14: Optimal model:
-  x            =  0 :: Integer
-  y            = 17 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 17 :: Integer
-  max_x_plus_y = 17 :: Integer
+  x            =   0 :: Integer
+  y            = -14 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -14 :: Integer
+  max_x_plus_y = -14 :: Integer
 Pareto front #15: Optimal model:
-  x            =  0 :: Integer
-  y            = 18 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 18 :: Integer
-  max_x_plus_y = 18 :: Integer
+  x            =   0 :: Integer
+  y            = -15 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -15 :: Integer
+  max_x_plus_y = -15 :: Integer
 Pareto front #16: Optimal model:
-  x            =  0 :: Integer
-  y            = 19 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 19 :: Integer
-  max_x_plus_y = 19 :: Integer
+  x            =   0 :: Integer
+  y            = -16 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -16 :: Integer
+  max_x_plus_y = -16 :: Integer
 Pareto front #17: Optimal model:
-  x            =  0 :: Integer
-  y            = 20 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 20 :: Integer
-  max_x_plus_y = 20 :: Integer
+  x            =   0 :: Integer
+  y            = -17 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -17 :: Integer
+  max_x_plus_y = -17 :: Integer
 Pareto front #18: Optimal model:
-  x            =  0 :: Integer
-  y            = 21 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 21 :: Integer
-  max_x_plus_y = 21 :: Integer
+  x            =   0 :: Integer
+  y            = -18 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -18 :: Integer
+  max_x_plus_y = -18 :: Integer
 Pareto front #19: Optimal model:
-  x            =  0 :: Integer
-  y            = 22 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 22 :: Integer
-  max_x_plus_y = 22 :: Integer
+  x            =   0 :: Integer
+  y            = -19 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -19 :: Integer
+  max_x_plus_y = -19 :: Integer
 Pareto front #20: Optimal model:
-  x            =  0 :: Integer
-  y            = 23 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 23 :: Integer
-  max_x_plus_y = 23 :: Integer
+  x            =   0 :: Integer
+  y            = -20 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -20 :: Integer
+  max_x_plus_y = -20 :: Integer
 Pareto front #21: Optimal model:
-  x            =  0 :: Integer
-  y            = 24 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 24 :: Integer
-  max_x_plus_y = 24 :: Integer
+  x            =   0 :: Integer
+  y            = -21 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -21 :: Integer
+  max_x_plus_y = -21 :: Integer
 Pareto front #22: Optimal model:
-  x            =  0 :: Integer
-  y            = 25 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 25 :: Integer
-  max_x_plus_y = 25 :: Integer
+  x            =   0 :: Integer
+  y            = -22 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -22 :: Integer
+  max_x_plus_y = -22 :: Integer
 Pareto front #23: Optimal model:
-  x            =  0 :: Integer
-  y            = 26 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 26 :: Integer
-  max_x_plus_y = 26 :: Integer
+  x            =   0 :: Integer
+  y            = -23 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -23 :: Integer
+  max_x_plus_y = -23 :: Integer
 Pareto front #24: Optimal model:
-  x            =  0 :: Integer
-  y            = 27 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = 27 :: Integer
-  max_x_plus_y = 27 :: Integer
+  x            =   0 :: Integer
+  y            = -24 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -24 :: Integer
+  max_x_plus_y = -24 :: Integer
 Pareto front #25: Optimal model:
-  x            = 0 :: Integer
-  y            = 3 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 3 :: Integer
-  max_x_plus_y = 3 :: Integer
+  x            =   0 :: Integer
+  y            = -25 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -25 :: Integer
+  max_x_plus_y = -25 :: Integer
 Pareto front #26: Optimal model:
-  x            = 0 :: Integer
-  y            = 2 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 2 :: Integer
-  max_x_plus_y = 2 :: Integer
+  x            =   0 :: Integer
+  y            = -26 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -26 :: Integer
+  max_x_plus_y = -26 :: Integer
 Pareto front #27: Optimal model:
-  x            = 0 :: Integer
-  y            = 1 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 1 :: Integer
-  max_x_plus_y = 1 :: Integer
+  x            =   0 :: Integer
+  y            = -27 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -27 :: Integer
+  max_x_plus_y = -27 :: Integer
 Pareto front #28: Optimal model:
-  x            = 0 :: Integer
-  y            = 0 :: Integer
-  min_x        = 0 :: Integer
-  max_y        = 0 :: Integer
-  max_x_plus_y = 0 :: Integer
+  x            =   0 :: Integer
+  y            = -28 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -28 :: Integer
+  max_x_plus_y = -28 :: Integer
 Pareto front #29: Optimal model:
-  x            =  0 :: Integer
-  y            = -1 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = -1 :: Integer
-  max_x_plus_y = -1 :: Integer
+  x            =   0 :: Integer
+  y            = -29 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -29 :: Integer
+  max_x_plus_y = -29 :: Integer
 Pareto front #30: Optimal model:
-  x            =  0 :: Integer
-  y            = -2 :: Integer
-  min_x        =  0 :: Integer
-  max_y        = -2 :: Integer
-  max_x_plus_y = -2 :: Integer
-*** Note: Pareto-front extraction was terminated before stream was ended as requested by the user.
-***       There might be other (potentially infinitely more) results.
+  x            =   0 :: Integer
+  y            = -30 :: Integer
+  min_x        =   0 :: Integer
+  max_y        = -30 :: Integer
+  max_x_plus_y = -30 :: Integer
+*** Note: Pareto-front extraction was terminated as requested by the user.
+***       There might be many other results!
diff --git a/SBVTestSuite/GoldFiles/pareto3.gold b/SBVTestSuite/GoldFiles/pareto3.gold
new file mode 100644
--- /dev/null
+++ b/SBVTestSuite/GoldFiles/pareto3.gold
@@ -0,0 +1,8 @@
+Pareto front #1: Optimal model:
+  x            = 0 :: Integer
+  min_x        = 0 :: Integer
+  max_x_plus_x = 0 :: Integer
+Pareto front #2: Optimal model:
+  x            = 1 :: Integer
+  min_x        = 1 :: Integer
+  max_x_plus_x = 2 :: Integer
diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold
--- a/SBVTestSuite/GoldFiles/query1.gold
+++ b/SBVTestSuite/GoldFiles/query1.gold
@@ -76,7 +76,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "state of the most recent check-sat command is not known")
 [SEND] (get-info :version)
-[RECV] (:version "4.7.0")
+[RECV] (:version "4.8.0")
 [SEND] (get-info :status)
 [RECV] (:status sat)
 [GOOD] (define-fun s16 () Int 4)
@@ -107,7 +107,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "unknown")
 [SEND] (get-info :version)
-[RECV] (:version "4.7.0")
+[RECV] (:version "4.8.0")
 [SEND] (get-info :memory)
 [RECV] unsupported
 [SEND] (get-info :time)
diff --git a/SBVTestSuite/GoldFiles/query_Interpolant1.gold b/SBVTestSuite/GoldFiles/query_Interpolant1.gold
--- a/SBVTestSuite/GoldFiles/query_Interpolant1.gold
+++ b/SBVTestSuite/GoldFiles/query_Interpolant1.gold
@@ -1,8 +1,8 @@
-** Calling: z3 -nw -in -smt2
+** Calling: mathsat -input=smt2 -theory.fp.minmax_zero_mode=4
 [GOOD] ; Automatically generated by SBV. Do not edit.
 [GOOD] (set-option :print-success true)
-[GOOD] (set-option :global-declarations true)
-[GOOD] (set-option :smtlib2_compliant true)
+** Backend solver MathSAT does not support global decls.
+** Some incremental calls, such as pop, will be limited.
 [GOOD] (set-option :diagnostic-output-channel "stdout")
 [GOOD] (set-option :produce-interpolants true)
 [GOOD] (set-option :produce-models true)
@@ -29,15 +29,14 @@
 [GOOD] (define-fun s8 () Bool (= s2 s3))
 [GOOD] (define-fun s9 () Bool (not s8))
 [GOOD] (define-fun s10 () Bool (and s7 s9))
-[GOOD] (assert (! s6 :named |c1|))
-[GOOD] (assert (! s10 :named |c2|))
+[GOOD] (assert (! s6 :interpolation-group |c1|))
+[GOOD] (assert (! s10 :interpolation-group |c2|))
 [SEND] (check-sat)
 [RECV] unsat
-[SEND] (get-interpolant |c1| |c2|)
-[RECV] (interpolants
-        (= s1 s2))
-*** Solver   : Z3
+[SEND] (get-interpolant (|c1|))
+[RECV] (= s1 s2)
+*** Solver   : MathSAT
 *** Exit code: ExitSuccess
 
 FINAL OUTPUT:
-["(= s1 s2)"]
+"(= s1 s2)"
diff --git a/SBVTestSuite/GoldFiles/query_Interpolant2.gold b/SBVTestSuite/GoldFiles/query_Interpolant2.gold
--- a/SBVTestSuite/GoldFiles/query_Interpolant2.gold
+++ b/SBVTestSuite/GoldFiles/query_Interpolant2.gold
@@ -1,8 +1,8 @@
-** Calling: z3 -nw -in -smt2
+** Calling: mathsat -input=smt2 -theory.fp.minmax_zero_mode=4
 [GOOD] ; Automatically generated by SBV. Do not edit.
 [GOOD] (set-option :print-success true)
-[GOOD] (set-option :global-declarations true)
-[GOOD] (set-option :smtlib2_compliant true)
+** Backend solver MathSAT does not support global decls.
+** Some incremental calls, such as pop, will be limited.
 [GOOD] (set-option :diagnostic-output-channel "stdout")
 [GOOD] (set-option :produce-interpolants true)
 [GOOD] (set-option :produce-models true)
@@ -34,15 +34,14 @@
 [GOOD] (define-fun s11 () Int (g s3))
 [GOOD] (define-fun s12 () Bool (distinct s10 s11))
 [GOOD] (define-fun s13 () Bool (and s9 s12))
-[GOOD] (assert (! s8 :named |c1|))
-[GOOD] (assert (! s13 :named |c2|))
+[GOOD] (assert (! s8 :interpolation-group |c1|))
+[GOOD] (assert (! s13 :interpolation-group |c2|))
 [SEND] (check-sat)
 [RECV] unsat
-[SEND] (get-interpolant |c1| |c2|)
-[RECV] (interpolants
-        (or (= s2 s3) (not (= s1 s0))))
-*** Solver   : Z3
+[SEND] (get-interpolant (|c1|))
+[RECV] (not (and (= s0 s1) (not (= s2 s3))))
+*** Solver   : MathSAT
 *** Exit code: ExitSuccess
 
 FINAL OUTPUT:
-["(or (= s2 s3) (not (= s1 s0)))"]
+"(not (and (= s0 s1) (not (= s2 s3))))"
diff --git a/SBVTestSuite/GoldFiles/query_Interpolant3.gold b/SBVTestSuite/GoldFiles/query_Interpolant3.gold
deleted file mode 100644
--- a/SBVTestSuite/GoldFiles/query_Interpolant3.gold
+++ /dev/null
@@ -1,49 +0,0 @@
-** Calling: z3 -nw -in -smt2
-[GOOD] ; Automatically generated by SBV. Do not edit.
-[GOOD] (set-option :print-success true)
-[GOOD] (set-option :global-declarations true)
-[GOOD] (set-option :smtlib2_compliant true)
-[GOOD] (set-option :diagnostic-output-channel "stdout")
-[GOOD] (set-option :produce-interpolants true)
-[GOOD] (set-option :produce-models true)
-[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
-[GOOD] ; --- uninterpreted sorts ---
-[GOOD] ; --- literal constants ---
-[GOOD] (define-fun s_2 () Bool false)
-[GOOD] (define-fun s_1 () Bool true)
-[GOOD] (define-fun s3 () Int 0)
-[GOOD] (define-fun s7 () Int 1)
-[GOOD] ; --- skolem constants ---
-[GOOD] (declare-fun s0 () Int) ; tracks user variable "x"
-[GOOD] (declare-fun s1 () Int) ; tracks user variable "y"
-[GOOD] (declare-fun s2 () Int) ; tracks user variable "z"
-[GOOD] ; --- constant tables ---
-[GOOD] ; --- skolemized tables ---
-[GOOD] ; --- arrays ---
-[GOOD] (declare-fun array_0 () (Array Int Int))
-[GOOD] (declare-fun array_1 () (Array Int Int))
-[GOOD] (declare-fun array_2 () (Array Int Int))
-[GOOD] (declare-fun array_3 () (Array Int Int))
-[GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- user given axioms ---
-[GOOD] ; --- formula ---
-[GOOD] (define-fun s4 () Bool (= array_1 array_3))
-[GOOD] (define-fun s5 () Bool (= s0 s2))
-[GOOD] (define-fun s6 () Int (select array_1 s2))
-[GOOD] (define-fun s8 () Bool (= s6 s7))
-[GOOD] (define-fun s9 () Bool (and s5 s8))
-[GOOD] (assert (= array_2 (store array_0 s0 s3)))
-[GOOD] (assert (= array_3 (store array_2 s1 s3)))
-[GOOD] (assert (! s4 :named |c1|))
-[GOOD] (assert (! s9 :named |c2|))
-[SEND] (check-sat)
-[RECV] unsat
-[SEND] (get-interpolant |c1| |c2|)
-[RECV] (interpolants
-        (and (= (select array_1 s0) (select (store array_2 s1 0) s0))
-            (or (= 0 (select array_1 s0)) (not (= s0 s1)))))
-*** Solver   : Z3
-*** Exit code: ExitSuccess
-
-FINAL OUTPUT:
-["(and (= (select array_1 s0) (select (store array_2 s1 0) s0)) (or (= 0 (select array_1 s0)) (not (= s0 s1))))"]
diff --git a/SBVTestSuite/GoldFiles/query_Interpolant4.gold b/SBVTestSuite/GoldFiles/query_Interpolant4.gold
deleted file mode 100644
--- a/SBVTestSuite/GoldFiles/query_Interpolant4.gold
+++ /dev/null
@@ -1,46 +0,0 @@
-** Calling: z3 -nw -in -smt2
-[GOOD] ; Automatically generated by SBV. Do not edit.
-[GOOD] (set-option :print-success true)
-[GOOD] (set-option :global-declarations true)
-[GOOD] (set-option :smtlib2_compliant true)
-[GOOD] (set-option :diagnostic-output-channel "stdout")
-[GOOD] (set-option :produce-interpolants true)
-[GOOD] (set-option :produce-models true)
-[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
-[GOOD] ; --- uninterpreted sorts ---
-[GOOD] ; --- literal constants ---
-[GOOD] (define-fun s_2 () Bool false)
-[GOOD] (define-fun s_1 () Bool true)
-[GOOD] ; --- skolem constants ---
-[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"
-[GOOD] (declare-fun s1 () Int) ; tracks user variable "b"
-[GOOD] (declare-fun s2 () Int) ; tracks user variable "c"
-[GOOD] (declare-fun s3 () Int) ; tracks user variable "d"
-[GOOD] (declare-fun s4 () Int) ; tracks user variable "e"
-[GOOD] ; --- constant tables ---
-[GOOD] ; --- skolemized tables ---
-[GOOD] ; --- arrays ---
-[GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- user given axioms ---
-[GOOD] ; --- formula ---
-[GOOD] (define-fun s5 () Bool (= s0 s1))
-[GOOD] (define-fun s6 () Bool (= s0 s2))
-[GOOD] (define-fun s7 () Bool (and s5 s6))
-[GOOD] (define-fun s8 () Bool (= s2 s3))
-[GOOD] (define-fun s9 () Bool (= s1 s4))
-[GOOD] (define-fun s10 () Bool (distinct s3 s4))
-[GOOD] (define-fun s11 () Bool (and s9 s10))
-[GOOD] (assert (! s7 :named |c1|))
-[GOOD] (assert (! s8 :named |c2|))
-[GOOD] (assert (! s11 :named |c3|))
-[SEND] (check-sat)
-[RECV] unsat
-[SEND] (get-interpolant |c1| |c2| |c3|)
-[RECV] (interpolants
-        (= s1 s2)
-        (= s1 s3))
-*** Solver   : Z3
-*** Exit code: ExitSuccess
-
-FINAL OUTPUT:
-["(= s1 s2)","(= s1 s3)"]
diff --git a/SBVTestSuite/GoldFiles/safe1.gold b/SBVTestSuite/GoldFiles/safe1.gold
new file mode 100644
--- /dev/null
+++ b/SBVTestSuite/GoldFiles/safe1.gold
@@ -0,0 +1,39 @@
+** Calling: z3 -nw -in -smt2
+[GOOD] ; Automatically generated by SBV. Do not edit.
+[GOOD] (set-option :print-success true)
+[GOOD] (set-option :global-declarations true)
+[GOOD] (set-option :smtlib2_compliant true)
+[GOOD] (set-option :diagnostic-output-channel "stdout")
+[GOOD] (set-option :produce-models true)
+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s_2 () Bool false)
+[GOOD] (define-fun s_1 () Bool true)
+[GOOD] (define-fun s1 () Int 12)
+[GOOD] (define-fun s3 () Int 2)
+[GOOD] ; --- skolem constants ---
+[GOOD] (declare-fun s0 () Int)
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- skolemized tables ---
+[GOOD] ; --- arrays ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user given axioms ---
+[GOOD] ; --- formula ---
+[GOOD] (define-fun s2 () Bool (= s0 s1))
+[GOOD] (define-fun s4 () Bool (> s0 s3))
+[GOOD] (define-fun s5 () Bool (not s4))
+[GOOD] (assert s_1)
+[GOOD] (push 1)
+[GOOD] (assert s5)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 0))
+[GOOD] (pop 1)
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+ FINAL: [safe1: Violated. Model:
+  s0 = 0 :: Integer]
+DONE!
diff --git a/SBVTestSuite/GoldFiles/safe2.gold b/SBVTestSuite/GoldFiles/safe2.gold
new file mode 100644
--- /dev/null
+++ b/SBVTestSuite/GoldFiles/safe2.gold
@@ -0,0 +1,38 @@
+** Calling: z3 -nw -in -smt2
+[GOOD] ; Automatically generated by SBV. Do not edit.
+[GOOD] (set-option :print-success true)
+[GOOD] (set-option :global-declarations true)
+[GOOD] (set-option :smtlib2_compliant true)
+[GOOD] (set-option :diagnostic-output-channel "stdout")
+[GOOD] (set-option :produce-models true)
+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s_2 () Bool false)
+[GOOD] (define-fun s_1 () Bool true)
+[GOOD] (define-fun s1 () Int 12)
+[GOOD] (define-fun s2 () Int 2)
+[GOOD] ; --- skolem constants ---
+[GOOD] (declare-fun s0 () Int)
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- skolemized tables ---
+[GOOD] ; --- arrays ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user given axioms ---
+[GOOD] ; --- formula ---
+[GOOD] (define-fun s3 () Bool (> s0 s2))
+[GOOD] (define-fun s4 () Bool (not s3))
+[GOOD] (assert s_1)
+[GOOD] (push 1)
+[GOOD] (assert s4)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 0))
+[GOOD] (pop 1)
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+ FINAL: [safe2: Violated. Model:
+  s0 = 0 :: Integer]
+DONE!
diff --git a/SBVTestSuite/GoldFiles/timeout1.gold b/SBVTestSuite/GoldFiles/timeout1.gold
--- a/SBVTestSuite/GoldFiles/timeout1.gold
+++ b/SBVTestSuite/GoldFiles/timeout1.gold
@@ -1,2 +1,2 @@
 Unknown.
-  Reason: canceled
+  Reason: timeout
diff --git a/SBVTestSuite/SBVDocTest.hs b/SBVTestSuite/SBVDocTest.hs
--- a/SBVTestSuite/SBVDocTest.hs
+++ b/SBVTestSuite/SBVDocTest.hs
@@ -10,28 +10,52 @@
 
 import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..), CIOS(..))
 
+import System.Random (randomRIO)
+
 main :: IO ()
 main = do (testEnv, testPercentage) <- getTestEnvironment
 
           putStrLn $ "SBVDocTest: Test platform: " ++ show testEnv
 
           case testEnv of
-            TestEnvLocal   -> runDocTest False
+            TestEnvLocal   -> runDocTest False False 100
             TestEnvCI env  -> if testPercentage < 50
                               then do putStrLn $ "Test percentage below tresheold, skipping doctest: " ++ show testPercentage
                                       exitSuccess
-                              else runDocTest (env == CIWindows)
+                              else runDocTest (env == CIWindows) True testPercentage
             TestEnvUnknown  -> do putStrLn "Unknown test environment, skipping doctests"
                                   exitSuccess
- where runDocTest windowsSkip = do srcFiles <- glob "Data/SBV/**/*.hs"
-                                   docFiles <- glob "Documentation/SBV/**/*.hs"
-                                   let allFiles = srcFiles ++ docFiles
-                                       testFiles
-                                         | windowsSkip = filter (not . bad) allFiles
-                                         | True        = allFiles
-                                   doctest testFiles
 
-       -- The following test has a path encoded in its output, and hence fails on Windows
-       -- since it has the c:\blah\blah format. Skip it:
-       bad fn = "nodiv0.hs" `isSuffixOf` map toLower fn
+ where runDocTest onWindows onRemote tp = do srcFiles <- glob "Data/SBV/**/*.hs"
+                                             docFiles <- glob "Documentation/SBV/**/*.hs"
 
+                                             let allFiles  = srcFiles ++ docFiles
+                                                 testFiles = filter (\nm -> not (skipWindows nm || skipRemote nm)) allFiles
+
+                                                 args = ["--fast", "--no-magic"]
+
+                                             tfs <- pickPercentage tp testFiles
+
+                                             doctest $ args ++ tfs
+
+         where skipWindows nm
+                 | not onWindows = False
+                 | True          = -- The following test has a path encoded in its output, and hence fails on Windows
+                                   -- since it has the c:\blah\blah format. Skip it:
+                                   "nodiv0.hs" `isSuffixOf` map toLower nm
+
+               skipRemote nm
+                 | not onRemote = False
+                 | True         = any (`isSuffixOf` map toLower nm) $ map (map toLower) skipList
+                 where skipList = [ "Interpolants.hs"  -- The following test requires mathSAT, so can't run on remote
+                                  , "HexPuzzle.hs"     -- Doctest is way too slow on this with ghci loading, sigh
+                                  , "MultMask.hs"      -- Also, quite slow
+                                  ]
+
+-- Pick (about) the given percentage of files
+pickPercentage :: Int -> [String] -> IO [String]
+pickPercentage 100 xs = return xs
+pickPercentage   0 _  = return []
+pickPercentage   p xs = concat <$> mapM pick xs
+  where pick f = do c <- randomRIO (0, 100)
+                    return [f | c >= p]
diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs
--- a/SBVTestSuite/SBVTest.hs
+++ b/SBVTestSuite/SBVTest.hs
@@ -12,6 +12,7 @@
 import qualified TestSuite.Basics.AllSat
 import qualified TestSuite.Basics.ArithNoSolver
 import qualified TestSuite.Basics.ArithSolver
+import qualified TestSuite.Basics.Assert
 import qualified TestSuite.Basics.BasicTests
 import qualified TestSuite.Basics.Exceptions
 import qualified TestSuite.Basics.GenBenchmark
@@ -54,6 +55,8 @@
 import qualified TestSuite.Optimization.ExtensionField
 import qualified TestSuite.Optimization.Quantified
 import qualified TestSuite.Optimization.Reals
+import qualified TestSuite.Overflows.Arithmetic
+import qualified TestSuite.Overflows.Casts
 import qualified TestSuite.Polynomials.Polynomials
 import qualified TestSuite.Puzzles.Coins
 import qualified TestSuite.Puzzles.Counts
@@ -125,8 +128,10 @@
                    , TestSuite.Queries.Int_CVC4.tests
                    , TestSuite.Queries.Int_Mathsat.tests
                    , TestSuite.Queries.Int_Yices.tests
-                   -- quick-check tests take a long time, so just run them locally.
+                   -- quick-check tests take a long time, so just run them locally:
                    , TestSuite.QuickCheck.QC.tests
+                   -- interpolant tests require MathSAT, run locally:
+                   , TestSuite.Queries.Interpolants.tests
                    ]
 
 -- | Remaining tests
@@ -136,6 +141,7 @@
                , TestSuite.Arrays.Query.tests
                , TestSuite.Basics.AllSat.tests
                , TestSuite.Basics.ArithNoSolver.tests
+               , TestSuite.Basics.Assert.tests
                , TestSuite.Basics.BasicTests.tests
                , TestSuite.Basics.Exceptions.testsRemote
                , TestSuite.Basics.GenBenchmark.tests
@@ -178,6 +184,8 @@
                , TestSuite.Optimization.ExtensionField.tests
                , TestSuite.Optimization.Quantified.tests
                , TestSuite.Optimization.Reals.tests
+               , TestSuite.Overflows.Arithmetic.tests
+               , TestSuite.Overflows.Casts.tests
                , TestSuite.Polynomials.Polynomials.tests
                , TestSuite.Puzzles.Coins.tests
                , TestSuite.Puzzles.Counts.tests
@@ -192,7 +200,6 @@
                , TestSuite.Queries.Enums.tests
                , TestSuite.Queries.FreshVars.tests
                , TestSuite.Queries.Int_Z3.tests
-               , TestSuite.Queries.Interpolants.tests
                , TestSuite.Queries.Strings.tests
                , TestSuite.Queries.Uninterpreted.tests
                , TestSuite.Uninterpreted.AUF.tests
diff --git a/SBVTestSuite/TestSuite/Basics/Assert.hs b/SBVTestSuite/TestSuite/Basics/Assert.hs
new file mode 100644
--- /dev/null
+++ b/SBVTestSuite/TestSuite/Basics/Assert.hs
@@ -0,0 +1,23 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  TestSuite.Basics.Assert
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Test the sAssert feature.
+-----------------------------------------------------------------------------
+
+module TestSuite.Basics.Assert(tests) where
+
+import Utils.SBVTestFramework
+
+-- Test suite
+tests :: TestTree
+tests = testGroup "Basics.Assert"
+   [ goldenCapturedIO "safe1" $ t $ \x -> sAssert Nothing "safe1" (x .> (2::SInteger)) (x .== 12)
+   , goldenCapturedIO "safe2" $ t $ \x -> sAssert Nothing "safe2" (x .> (2::SInteger)) (12::SInteger)
+   ]
+   where t tc goldFile = do r <- safeWith z3{verbose=True, redirectVerbose=Just goldFile} tc
+                            appendFile goldFile ("\n FINAL: " ++ show r ++ "\nDONE!")
diff --git a/SBVTestSuite/TestSuite/Optimization/Combined.hs b/SBVTestSuite/TestSuite/Optimization/Combined.hs
--- a/SBVTestSuite/TestSuite/Optimization/Combined.hs
+++ b/SBVTestSuite/TestSuite/Optimization/Combined.hs
@@ -21,6 +21,7 @@
     , goldenVsStringShow "combined2" (optimize Lexicographic      combined2)
     , goldenVsStringShow "pareto1"   (optimize (Pareto Nothing)   pareto1)
     , goldenVsStringShow "pareto2"   (optimize (Pareto (Just 30)) pareto2)
+    , goldenVsStringShow "pareto3"   (optimize (Pareto Nothing)   pareto3)
     , goldenVsStringShow "boxed1"    (optimize Independent        boxed1)
     ]
 
@@ -72,6 +73,15 @@
              minimize "min_x"            x
              maximize "max_y"            y
              minimize "max_x_plus_y"   $ x + y
+
+pareto3 :: Goal
+pareto3 = do x <- sInteger "x"
+
+             constrain $ 1 .>= x
+             constrain $ 0 .<= x
+
+             minimize "min_x"            x
+             maximize "max_x_plus_x"   $ x + x
 
 boxed1 :: Goal
 boxed1 = do x <- sReal "x"
diff --git a/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs b/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs
new file mode 100644
--- /dev/null
+++ b/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs
@@ -0,0 +1,246 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  TestSuite.Overflows.Arithmetic
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Test suite for overflow checking
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE Rank2Types          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module TestSuite.Overflows.Arithmetic(tests) where
+
+import Data.SBV
+import Data.SBV.Dynamic
+import Data.SBV.Internals (unSBV, SBV(..))
+
+import Data.SBV.Tools.Overflow
+
+import Utils.SBVTestFramework
+
+-- Test suite
+tests :: TestTree
+tests = testGroup "Overflows" [testGroup "Arithmetic" ts]
+  where ts = [ testGroup "add-uf" [ testCase "w8"  $ assertIsThm $ underflow  svPlus     (bvAddO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ underflow  svPlus     (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ underflow  svPlus     (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ underflow  svPlus     (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ underflow  svPlus     (bvAddO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ underflow  svPlus     (bvAddO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ underflow  svPlus     (bvAddO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ underflow  svPlus     (bvAddO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "add-of" [ testCase "w8"  $ assertIsThm $ overflow   svPlus     (bvAddO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ overflow   svPlus     (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ overflow   svPlus     (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ overflow   svPlus     (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ overflow   svPlus     (bvAddO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ overflow   svPlus     (bvAddO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ overflow   svPlus     (bvAddO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ overflow   svPlus     (bvAddO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "sub-uf" [ testCase "w8"  $ assertIsThm $ underflow  svMinus    (bvSubO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ underflow  svMinus    (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ underflow  svMinus    (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ underflow  svMinus    (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ underflow  svMinus    (bvSubO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ underflow  svMinus    (bvSubO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ underflow  svMinus    (bvSubO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ underflow  svMinus    (bvSubO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "sub-of" [ testCase "w8"  $ assertIsThm $ overflow   svMinus    (bvSubO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ overflow   svMinus    (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ overflow   svMinus    (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ overflow   svMinus    (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ overflow   svMinus    (bvSubO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ overflow   svMinus    (bvSubO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ overflow   svMinus    (bvSubO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ overflow   svMinus    (bvSubO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "mul-uf" [ testCase "w8"  $ assertIsThm $ underflow  svTimes    (bvMulO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ underflow  svTimes    (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ underflow  svTimes    (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ underflow  svTimes    (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ mulChkU    bvMulOFast (bvMulO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ mulChkU    bvMulOFast (bvMulO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ mulChkU    bvMulOFast (bvMulO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ mulChkU    bvMulOFast (bvMulO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "mul-of" [ testCase "w8"  $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ mulChkO    bvMulOFast (bvMulO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "div-uf" [ testCase "w8"  $ assertIsThm $ never      svDivide    (bvDivO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ never      svDivide    (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ never      svDivide    (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ never      svDivide    (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ never      svDivide    (bvDivO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ never      svDivide    (bvDivO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ never      svDivide    (bvDivO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ never      svDivide    (bvDivO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "div-of" [ testCase "w8"  $ assertIsThm $ never      svDivide    (bvDivO :: SWord8  -> SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ never      svDivide    (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ never      svDivide    (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ never      svDivide    (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ divChk     svDivide    (bvDivO :: SInt8   -> SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ divChk     svDivide    (bvDivO :: SInt16  -> SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ divChk     svDivide    (bvDivO :: SInt32  -> SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ divChk     svDivide    (bvDivO :: SInt64  -> SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "neg-uf" [ testCase "w8"  $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ underflow1 svNeg0      (bvNegO :: SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ underflow1 svNeg0      (bvNegO :: SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ underflow1 svNeg0      (bvNegO :: SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ underflow1 svNeg0      (bvNegO :: SInt64  -> (SBool, SBool))
+                                  ]
+             , testGroup "neg-of" [ testCase "w8"  $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord8  -> (SBool, SBool))
+                                  , testCase "w16" $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord16 -> (SBool, SBool))
+                                  , testCase "w32" $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord32 -> (SBool, SBool))
+                                  , testCase "w64" $ assertIsThm $ never1     svNeg0      (bvNegO :: SWord64 -> (SBool, SBool))
+                                  , testCase "i8"  $ assertIsThm $ overflow1  svNeg0      (bvNegO :: SInt8   -> (SBool, SBool))
+                                  , testCase "i16" $ assertIsThm $ overflow1  svNeg0      (bvNegO :: SInt16  -> (SBool, SBool))
+                                  , testCase "i32" $ assertIsThm $ overflow1  svNeg0      (bvNegO :: SInt32  -> (SBool, SBool))
+                                  , testCase "i64" $ assertIsThm $ overflow1  svNeg0      (bvNegO :: SInt64  -> (SBool, SBool))
+                                  ]
+             ]
+
+-- 256 bits is large enough to do all these proofs
+large :: Int
+large = 256
+
+type SLarge = SVal
+
+svNeg0 :: SLarge -> SLarge
+svNeg0 v = z `svMinus` v
+  where z = svInteger (KBounded (hasSign v) large) 0
+
+exactlyWhen :: SBool -> SVal -> SBool
+exactlyWhen (SBV a) b = SBV $ (a `svAnd` b) `svOr` (svNot a `svAnd` svNot b)
+
+-- Properly extend to a dynamic large vector
+toLarge :: SBV a -> SLarge
+toLarge v
+  | extra < 0 = error $ "toLarge: Unexpected size: " ++ show (n, large)
+  | hasSign v = p `svJoin` dv
+  | True      = z `svJoin` dv
+  where n     = intSizeOf v
+        extra = large - n
+
+        dv    = unSBV v
+        mk    = svInteger (KBounded True extra)
+        z     = mk 0
+        o     = mk (-1)
+        pos   = (dv `svTestBit` (n-1)) `svEqual` svFalse
+        p     = svIte pos z o
+
+-- Multiplication checks are expensive. For these, we simply check that the SBV encodings and the z3 versions are equivalent
+mulChkO :: forall a. (SymWord a) => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
+mulChkO fast slow = do setLogic Logic_NONE
+                       x <- free "x"
+                       y <- free "y"
+
+                       let (_, ov1) = x `fast` y
+                           (_, ov2) = x `slow` y
+
+                       return $ ov1 .== ov2
+
+-- Underflow mults
+mulChkU :: forall a. (SymWord a) => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
+mulChkU fast slow = do setLogic Logic_NONE
+                       x <- free "x"
+                       y <- free "y"
+
+                       let (uf1, _) = x `fast` y
+                           (uf2, _) = x `slow` y
+
+                       return $ uf1 .== uf2
+
+-- Signed division can only underflow under one condition, check that simply instead of trying to do an expensive embedding proof
+divChk :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
+divChk _op cond = do x  <- free "x"
+                     y  <- free "y"
+
+                     let (_, overflowHappens) = x `cond` y
+
+                         special = (unSBV x `svEqual` topSet) `svAnd` (unSBV y `svEqual` neg1)
+
+                         n      = intSizeOf x
+                         neg1   = svInteger (KBounded True n) (-1)
+                         topSet = svInteger (KBounded True n) (2^(n-1))
+
+                     return $ overflowHappens `exactlyWhen` special
+
+-- For a few cases, we expect them to "never" overflow. The "embedding proofs" are either too expensive (in case of division), or
+-- not possible (in case of negation). We capture these here.
+never :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
+never _op cond = do x  <- free "x"
+                    y  <- free "y"
+
+                    let (underflowHappens, _) = x `cond` y
+
+                    return $ underflowHappens `exactlyWhen` svFalse
+
+never1 :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate
+never1 _op cond = do x  <- free "x"
+
+                     let (underflowHappens, _) = cond x
+
+                     return $ underflowHappens `exactlyWhen` svFalse
+
+underflow :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
+underflow op cond = do x  <- free "x"
+                       y  <- free "y"
+
+                       let (underflowHappens, _) = x `cond` y
+
+                           extResult :: SLarge
+                           extResult = toLarge x `op` toLarge y
+
+
+                       return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a))
+
+overflow :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
+overflow op cond = do x  <- free "x"
+                      y  <- free "y"
+
+                      let (_, overflowHappens) = x `cond` y
+
+                          extResult :: SLarge
+                          extResult = toLarge x `op` toLarge y
+
+                      return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a))
+
+underflow1 :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate
+underflow1 op cond = do x  <- free "x"
+
+                        let (underflowHappens, _) = cond x
+
+                            extResult :: SLarge
+                            extResult = op $ toLarge x
+
+                        return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a))
+
+overflow1 :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate
+overflow1 op cond = do x  <- free "x"
+
+                       let (_, overflowHappens) = cond x
+
+                           extResult :: SLarge
+                           extResult = op $ toLarge x
+
+                       return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a))
+
+{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
diff --git a/SBVTestSuite/TestSuite/Overflows/Casts.hs b/SBVTestSuite/TestSuite/Overflows/Casts.hs
new file mode 100644
--- /dev/null
+++ b/SBVTestSuite/TestSuite/Overflows/Casts.hs
@@ -0,0 +1,134 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  TestSuite.Overflows.Casts
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Test suite for overflow checking
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE Rank2Types          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module TestSuite.Overflows.Casts(tests) where
+
+import Data.SBV
+import Data.SBV.Tools.Overflow
+
+import Utils.SBVTestFramework
+
+type C a b = SBV a -> (SBV b, (SBool, SBool))
+
+getBounds :: (Bounded a, Integral a) => a -> Maybe (Integer, Integer)
+getBounds x = Just (fromIntegral (minBound `asTypeOf` x), fromIntegral (maxBound `asTypeOf` x))
+
+-- Test suite
+tests :: TestTree
+tests = testGroup "Overflows" [testGroup "Casts" ts]
+  where ts = [ testGroup "w8"  [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word8   Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word8   Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word8   Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word8   Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Word8   Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word8   Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word8   Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word8   Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Word8   Integer)
+                               ]
+             , testGroup "w16" [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word16  Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word16  Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word16  Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word16  Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Word16  Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word16  Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word16  Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word16  Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Word16  Integer)
+                               ]
+             , testGroup "w32" [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word32  Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word32  Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word32  Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word32  Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Word32  Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word32  Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word32  Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word32  Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Word32  Integer)
+                               ]
+             , testGroup "w64" [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word64  Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word64  Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word64  Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word64  Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Word64  Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word64  Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word64  Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word64  Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Word64  Integer)
+                               ]
+             , testGroup "i8"  [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int8    Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int8    Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int8    Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int8    Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Int8    Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int8    Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int8    Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int8    Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Int8    Integer)
+                               ]
+             , testGroup "i16" [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int16   Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int16   Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int16   Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int16   Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Int16   Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int16   Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int16   Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int16   Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Int16   Integer)
+                               ]
+             , testGroup "i32" [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int32   Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int32   Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int32   Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int32   Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Int32   Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int32   Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int32   Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int32   Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Int32   Integer)
+                               ]
+             , testGroup "i64" [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int64   Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int64   Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int64   Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int64   Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Int64   Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int64   Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int64   Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int64   Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Int64   Integer)
+                               ]
+             , testGroup "i"   [ testCase "w8"  $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Integer Word8)
+                               , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Integer Word16)
+                               , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Integer Word32)
+                               , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Integer Word64)
+                               , testCase "i8"  $ assertIsThm $ chk (getBounds (undefined :: Int8  )) (sFromIntegralO :: C Integer Int8)
+                               , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Integer Int16)
+                               , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Integer Int32)
+                               , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Integer Int64)
+                               , testCase "i"   $ assertIsThm $ chk Nothing                           (sFromIntegralO :: C Integer Integer)
+                               ]
+             ]
+
+chk :: forall a b. (SymWord a, SymWord b, Integral a, Integral b) => Maybe (Integer, Integer) -> (SBV a -> (SBV b, (SBool, SBool))) -> Predicate
+chk mb cvt = do (x :: SBV a) <- free "x"
+
+                let (_ :: SBV b, (uf, ov)) = cvt x
+
+                    ix :: SInteger
+                    ix = sFromIntegral x
+
+                    (ufCorrect, ovCorrect) = case mb of
+                                               Nothing       -> (uf .== false,            ov .== false)
+                                               Just (lb, ub) -> (uf <=> ix .< literal lb, ov <=> ix .> literal ub)
+
+                return $ ufCorrect &&& ovCorrect
diff --git a/SBVTestSuite/TestSuite/Queries/Interpolants.hs b/SBVTestSuite/TestSuite/Queries/Interpolants.hs
--- a/SBVTestSuite/TestSuite/Queries/Interpolants.hs
+++ b/SBVTestSuite/TestSuite/Queries/Interpolants.hs
@@ -7,6 +7,7 @@
 -- Stability   :  experimental
 --
 -- Testing a few interpolant computations.
+--
 -----------------------------------------------------------------------------
 {-# LANGUAGE ScopedTypeVariables #-}
 
@@ -22,15 +23,16 @@
   testGroup "Basics.QueryInterpolants"
     [ goldenCapturedIO "query_Interpolant1" $ testQuery q1
     , goldenCapturedIO "query_Interpolant2" $ testQuery q2
-    , goldenCapturedIO "query_Interpolant3" $ testQuery q3
-    , goldenCapturedIO "query_Interpolant4" $ testQuery q4
     ]
 
 testQuery :: Show a => Symbolic a -> FilePath -> IO ()
-testQuery t rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t
+testQuery t rf = do r <- runSMTWith mathSAT{verbose=True, redirectVerbose=Just rf} t
                     appendFile rf ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")
 
-q1 :: Symbolic [String]
+iConstraint :: String -> SBool -> Symbolic ()
+iConstraint g = constrainWithAttribute [(":interpolation-group", g)]
+
+q1 :: Symbolic String
 q1 = do a <- sInteger "a"
         b <- sInteger "b"
         c <- sInteger "c"
@@ -38,13 +40,13 @@
 
         setOption $ ProduceInterpolants True
 
-        namedConstraint "c1" $ a .== b &&& a .== c
-        namedConstraint "c2" $ b .== d &&& bnot (c .== d)
+        iConstraint "c1" $ a .== b &&& a .== c
+        iConstraint "c2" $ b .== d &&& bnot (c .== d)
 
         query $ do _ <- checkSat
-                   getInterpolant ["c1", "c2"]
+                   getInterpolant ["c1"]
 
-q2 :: Symbolic [String]
+q2 :: Symbolic String
 q2 = do a <- sInteger "a"
         b <- sInteger "b"
         c <- sInteger "c"
@@ -56,42 +58,10 @@
 
         setOption $ ProduceInterpolants True
 
-        namedConstraint "c1" $ f a .== c &&& f b .== d
-        namedConstraint "c2" $   a .== b &&& g c ./= g d
-
-        query $ do _ <- checkSat
-                   getInterpolant ["c1", "c2"]
-
-q3 :: Symbolic [String]
-q3 = do x <- sInteger "x"
-        y <- sInteger "y"
-        z <- sInteger "z"
-
-        a :: SArray Integer Integer <- newArray "a"
-        b :: SArray Integer Integer <- newArray "b"
-
-        namedConstraint "c1" $ b .== writeArray (writeArray a x 0) y (0::SInteger)
-        namedConstraint "c2" $ z .== x &&& readArray b z .== 1
-
-        setOption $ ProduceInterpolants True
-
-        query $ do _ <- checkSat
-                   getInterpolant ["c1", "c2"]
-
-q4 :: Symbolic [String]
-q4 = do a <- sInteger "a"
-        b <- sInteger "b"
-        c <- sInteger "c"
-        d <- sInteger "d"
-        e <- sInteger "e"
-
-        namedConstraint "c1" $ a .== b &&& a .== c
-        namedConstraint "c2" $ c .== d
-        namedConstraint "c3" $ b .== e &&& d ./= e
-
-        setOption $ ProduceInterpolants True
+        iConstraint "c1" $ f a .== c &&& f b .== d
+        iConstraint "c2" $   a .== b &&& g c ./= g d
 
         query $ do _ <- checkSat
-                   getInterpolant ["c1", "c2", "c3"]
+                   getInterpolant ["c1"]
 
 {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,5 +1,5 @@
 Name:          sbv
-Version:       7.8
+Version:       7.9
 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
@@ -61,6 +61,7 @@
                   , Data.SBV.RegExp
                   , Data.SBV.Tools.CodeGen
                   , Data.SBV.Tools.GenTest
+                  , Data.SBV.Tools.Overflow
                   , Data.SBV.Tools.Polynomial
                   , Data.SBV.Tools.STree
                   , Documentation.SBV.Examples.BitPrecise.BitTricks
@@ -168,6 +169,7 @@
                   , TestSuite.Basics.AllSat
                   , TestSuite.Basics.ArithNoSolver
                   , TestSuite.Basics.ArithSolver
+                  , TestSuite.Basics.Assert
                   , TestSuite.Basics.BasicTests
                   , TestSuite.Basics.Exceptions
                   , TestSuite.Basics.GenBenchmark
@@ -210,6 +212,8 @@
                   , TestSuite.Optimization.ExtensionField
                   , TestSuite.Optimization.Quantified
                   , TestSuite.Optimization.Reals
+                  , TestSuite.Overflows.Arithmetic
+                  , TestSuite.Overflows.Casts
                   , TestSuite.Polynomials.Polynomials
                   , TestSuite.Puzzles.Coins
                   , TestSuite.Puzzles.Counts
@@ -243,7 +247,7 @@
 
 Test-Suite SBVDocTest
     Build-Depends:    base, directory, filepath, random
-                    , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck
+                    , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, random
                     , sbv
     default-language: Haskell2010
     Hs-Source-Dirs  : SBVTestSuite