    -----------------------------------------------------------------------------
    -- |
    -- 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 FlexibleContexts     #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE ImplicitParams       #-}
    {-# LANGUAGE Rank2Types           #-}
    {-# LANGUAGE ScopedTypeVariables  #-}
    {-# LANGUAGE TypeApplications     #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.Overflow (

             -- * Arithmetic overflows
             ArithOverflow(..), CheckedArithmetic(..)

             -- * Cast overflows
           , sFromIntegralO, sFromIntegralChecked

        ) where

    import Data.SBV.Core.Data
    import Data.SBV.Core.Kind
    import Data.SBV.Core.Model
    import Data.SBV.Core.Operations
    import Data.SBV.Core.Sized

    import GHC.TypeLits

    import GHC.Stack

    import Data.Int
    import Data.Word
    import Data.Proxy

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    -- | 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 minimum 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 :: SWord8 -> SWord8 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SWord8 -> SWord8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SWord8 -> SWord8 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SWord8 -> SWord8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SWord8 -> SWord8 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SWord8 -> SWord8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SWord8 -> SWord8 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SWord8 -> SWord8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SWord8 -> SWord8 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SWord8 -> SWord8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SWord8 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SWord8 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance ArithOverflow SWord16 where {bvAddO :: SWord16 -> SWord16 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SWord16 -> SWord16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SWord16 -> SWord16 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SWord16 -> SWord16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SWord16 -> SWord16 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SWord16 -> SWord16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SWord16 -> SWord16 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SWord16 -> SWord16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SWord16 -> SWord16 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SWord16 -> SWord16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SWord16 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SWord16 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance ArithOverflow SWord32 where {bvAddO :: SWord32 -> SWord32 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SWord32 -> SWord32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SWord32 -> SWord32 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SWord32 -> SWord32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SWord32 -> SWord32 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SWord32 -> SWord32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SWord32 -> SWord32 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SWord32 -> SWord32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SWord32 -> SWord32 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SWord32 -> SWord32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SWord32 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SWord32 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance ArithOverflow SWord64 where {bvAddO :: SWord64 -> SWord64 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SWord64 -> SWord64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SWord64 -> SWord64 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SWord64 -> SWord64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SWord64 -> SWord64 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SWord64 -> SWord64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SWord64 -> SWord64 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SWord64 -> SWord64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SWord64 -> SWord64 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SWord64 -> SWord64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SWord64 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SWord64 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance ArithOverflow SInt8   where {bvAddO :: SInt8 -> SInt8 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SInt8 -> SInt8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SInt8 -> SInt8 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SInt8 -> SInt8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SInt8 -> SInt8 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SInt8 -> SInt8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SInt8 -> SInt8 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SInt8 -> SInt8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SInt8 -> SInt8 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SInt8 -> SInt8 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SInt8 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SInt8 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance ArithOverflow SInt16  where {bvAddO :: SInt16 -> SInt16 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SInt16 -> SInt16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SInt16 -> SInt16 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SInt16 -> SInt16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SInt16 -> SInt16 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SInt16 -> SInt16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SInt16 -> SInt16 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SInt16 -> SInt16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SInt16 -> SInt16 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SInt16 -> SInt16 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SInt16 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SInt16 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance ArithOverflow SInt32  where {bvAddO :: SInt32 -> SInt32 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SInt32 -> SInt32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SInt32 -> SInt32 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SInt32 -> SInt32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SInt32 -> SInt32 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SInt32 -> SInt32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SInt32 -> SInt32 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SInt32 -> SInt32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SInt32 -> SInt32 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SInt32 -> SInt32 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SInt32 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SInt32 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance ArithOverflow SInt64  where {bvAddO :: SInt64 -> SInt64 -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SInt64 -> SInt64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SInt64 -> SInt64 -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SInt64 -> SInt64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SInt64 -> SInt64 -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SInt64 -> SInt64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SInt64 -> SInt64 -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SInt64 -> SInt64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SInt64 -> SInt64 -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SInt64 -> SInt64 -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SInt64 -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SInt64 -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}

    instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SWord n) where {bvAddO :: SWord n -> SWord n -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SWord n -> SWord n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SWord n -> SWord n -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SWord n -> SWord n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SWord n -> SWord n -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SWord n -> SWord n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SWord n -> SWord n -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SWord n -> SWord n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SWord n -> SWord n -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SWord n -> SWord n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SWord n -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SWord n -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}
    instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt  n) where {bvAddO :: SInt n -> SInt n -> (SBool, SBool)
    bvAddO = (SVal -> SVal -> (SBool, SBool))
    -> SInt n -> SInt n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO; bvSubO :: SInt n -> SInt n -> (SBool, SBool)
    bvSubO = (SVal -> SVal -> (SBool, SBool))
    -> SInt n -> SInt n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO; bvMulO :: SInt n -> SInt n -> (SBool, SBool)
    bvMulO = (SVal -> SVal -> (SBool, SBool))
    -> SInt n -> SInt n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO; bvMulOFast :: SInt n -> SInt n -> (SBool, SBool)
    bvMulOFast = (SVal -> SVal -> (SBool, SBool))
    -> SInt n -> SInt n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulOFast; bvDivO :: SInt n -> SInt n -> (SBool, SBool)
    bvDivO = (SVal -> SVal -> (SBool, SBool))
    -> SInt n -> SInt n -> (SBool, SBool)
    forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO; bvNegO :: SInt n -> (SBool, SBool)
    bvNegO = (SVal -> (SBool, SBool)) -> SInt n -> (SBool, SBool)
    forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO}

    instance ArithOverflow SVal where
      bvAddO :: SVal -> SVal -> (SBool, SBool)
    bvAddO     = (Int -> SVal -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> SVal -> (SVal, SVal))
    -> SVal
    -> SVal
    -> (SBool, SBool)
    signPick2 Int -> SVal -> SVal -> (SVal, SVal)
    bvuaddo     Int -> SVal -> SVal -> (SVal, SVal)
    bvsaddo
      bvSubO :: SVal -> SVal -> (SBool, SBool)
    bvSubO     = (Int -> SVal -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> SVal -> (SVal, SVal))
    -> SVal
    -> SVal
    -> (SBool, SBool)
    signPick2 Int -> SVal -> SVal -> (SVal, SVal)
    bvusubo     Int -> SVal -> SVal -> (SVal, SVal)
    bvssubo
      bvMulO :: SVal -> SVal -> (SBool, SBool)
    bvMulO     = (Int -> SVal -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> SVal -> (SVal, SVal))
    -> SVal
    -> SVal
    -> (SBool, SBool)
    signPick2 Int -> SVal -> SVal -> (SVal, SVal)
    bvumulo     Int -> SVal -> SVal -> (SVal, SVal)
    bvsmulo
      bvMulOFast :: SVal -> SVal -> (SBool, SBool)
    bvMulOFast = (Int -> SVal -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> SVal -> (SVal, SVal))
    -> SVal
    -> SVal
    -> (SBool, SBool)
    signPick2 Int -> SVal -> SVal -> (SVal, SVal)
    bvumuloFast Int -> SVal -> SVal -> (SVal, SVal)
    bvsmuloFast
      bvDivO :: SVal -> SVal -> (SBool, SBool)
    bvDivO     = (Int -> SVal -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> SVal -> (SVal, SVal))
    -> SVal
    -> SVal
    -> (SBool, SBool)
    signPick2 Int -> SVal -> SVal -> (SVal, SVal)
    bvudivo     Int -> SVal -> SVal -> (SVal, SVal)
    bvsdivo
      bvNegO :: SVal -> (SBool, SBool)
    bvNegO     = (Int -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> (SVal, SVal)) -> SVal -> (SBool, SBool)
    signPick1 Int -> SVal -> (SVal, SVal)
    bvunego     Int -> SVal -> (SVal, SVal)
    bvsnego

    -- | A class of checked-arithmetic operations. These follow the usual arithmetic,
    -- except make calls to 'Data.SBV.sAssert' to ensure no overflow/underflow can occur.
    -- Use them in conjunction with 'Data.SBV.safe' to ensure no overflow can happen.
    class (ArithOverflow (SBV a), Num a, SymVal a) => CheckedArithmetic a where
      (+!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
      (-!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
      (*!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
      (/!)          :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
      negateChecked :: (?loc :: CallStack) => SBV a          -> SBV a

      infixl 6 +!, -!
      infixl 7 *!, /!

    instance CheckedArithmetic Word8 where
      +! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
    (+!)          = CallStack
    -> String
    -> (SWord8 -> SWord8 -> SWord8)
    -> (SWord8 -> SWord8 -> (SBool, SBool))
    -> SWord8
    -> SWord8
    -> SWord8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SWord8 -> SWord8 -> SWord8
    forall a. Num a => a -> a -> a
    (+)    SWord8 -> SWord8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
    (-!)          = CallStack
    -> String
    -> (SWord8 -> SWord8 -> SWord8)
    -> (SWord8 -> SWord8 -> (SBool, SBool))
    -> SWord8
    -> SWord8
    -> SWord8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SWord8 -> SWord8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
    (*!)          = CallStack
    -> String
    -> (SWord8 -> SWord8 -> SWord8)
    -> (SWord8 -> SWord8 -> (SBool, SBool))
    -> SWord8
    -> SWord8
    -> SWord8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SWord8 -> SWord8 -> SWord8
    forall a. Num a => a -> a -> a
    (*)    SWord8 -> SWord8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SWord8 -> SWord8 -> SWord8
    (/!)          = CallStack
    -> String
    -> (SWord8 -> SWord8 -> SWord8)
    -> (SWord8 -> SWord8 -> (SBool, SBool))
    -> SWord8
    -> SWord8
    -> SWord8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SWord8 -> SWord8 -> SWord8
    forall a. SDivisible a => a -> a -> a
    sDiv   SWord8 -> SWord8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SWord8 -> SWord8
    negateChecked = CallStack
    -> String
    -> (SWord8 -> SWord8)
    -> (SWord8 -> (SBool, SBool))
    -> SWord8
    -> SWord8
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SWord8 -> SWord8
    forall a. Num a => a -> a
    negate SWord8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance CheckedArithmetic Word16 where
      +! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
    (+!)          = CallStack
    -> String
    -> (SWord16 -> SWord16 -> SWord16)
    -> (SWord16 -> SWord16 -> (SBool, SBool))
    -> SWord16
    -> SWord16
    -> SWord16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SWord16 -> SWord16 -> SWord16
    forall a. Num a => a -> a -> a
    (+)    SWord16 -> SWord16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
    (-!)          = CallStack
    -> String
    -> (SWord16 -> SWord16 -> SWord16)
    -> (SWord16 -> SWord16 -> (SBool, SBool))
    -> SWord16
    -> SWord16
    -> SWord16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SWord16 -> SWord16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
    (*!)          = CallStack
    -> String
    -> (SWord16 -> SWord16 -> SWord16)
    -> (SWord16 -> SWord16 -> (SBool, SBool))
    -> SWord16
    -> SWord16
    -> SWord16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SWord16 -> SWord16 -> SWord16
    forall a. Num a => a -> a -> a
    (*)    SWord16 -> SWord16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SWord16 -> SWord16 -> SWord16
    (/!)          = CallStack
    -> String
    -> (SWord16 -> SWord16 -> SWord16)
    -> (SWord16 -> SWord16 -> (SBool, SBool))
    -> SWord16
    -> SWord16
    -> SWord16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SWord16 -> SWord16 -> SWord16
    forall a. SDivisible a => a -> a -> a
    sDiv   SWord16 -> SWord16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SWord16 -> SWord16
    negateChecked = CallStack
    -> String
    -> (SWord16 -> SWord16)
    -> (SWord16 -> (SBool, SBool))
    -> SWord16
    -> SWord16
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SWord16 -> SWord16
    forall a. Num a => a -> a
    negate SWord16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance CheckedArithmetic Word32 where
      +! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
    (+!)          = CallStack
    -> String
    -> (SWord32 -> SWord32 -> SWord32)
    -> (SWord32 -> SWord32 -> (SBool, SBool))
    -> SWord32
    -> SWord32
    -> SWord32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SWord32 -> SWord32 -> SWord32
    forall a. Num a => a -> a -> a
    (+)    SWord32 -> SWord32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
    (-!)          = CallStack
    -> String
    -> (SWord32 -> SWord32 -> SWord32)
    -> (SWord32 -> SWord32 -> (SBool, SBool))
    -> SWord32
    -> SWord32
    -> SWord32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SWord32 -> SWord32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
    (*!)          = CallStack
    -> String
    -> (SWord32 -> SWord32 -> SWord32)
    -> (SWord32 -> SWord32 -> (SBool, SBool))
    -> SWord32
    -> SWord32
    -> SWord32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SWord32 -> SWord32 -> SWord32
    forall a. Num a => a -> a -> a
    (*)    SWord32 -> SWord32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SWord32 -> SWord32 -> SWord32
    (/!)          = CallStack
    -> String
    -> (SWord32 -> SWord32 -> SWord32)
    -> (SWord32 -> SWord32 -> (SBool, SBool))
    -> SWord32
    -> SWord32
    -> SWord32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SWord32 -> SWord32 -> SWord32
    forall a. SDivisible a => a -> a -> a
    sDiv   SWord32 -> SWord32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SWord32 -> SWord32
    negateChecked = CallStack
    -> String
    -> (SWord32 -> SWord32)
    -> (SWord32 -> (SBool, SBool))
    -> SWord32
    -> SWord32
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SWord32 -> SWord32
    forall a. Num a => a -> a
    negate SWord32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance CheckedArithmetic Word64 where
      +! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
    (+!)          = CallStack
    -> String
    -> (SWord64 -> SWord64 -> SWord64)
    -> (SWord64 -> SWord64 -> (SBool, SBool))
    -> SWord64
    -> SWord64
    -> SWord64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SWord64 -> SWord64 -> SWord64
    forall a. Num a => a -> a -> a
    (+)    SWord64 -> SWord64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
    (-!)          = CallStack
    -> String
    -> (SWord64 -> SWord64 -> SWord64)
    -> (SWord64 -> SWord64 -> (SBool, SBool))
    -> SWord64
    -> SWord64
    -> SWord64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SWord64 -> SWord64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
    (*!)          = CallStack
    -> String
    -> (SWord64 -> SWord64 -> SWord64)
    -> (SWord64 -> SWord64 -> (SBool, SBool))
    -> SWord64
    -> SWord64
    -> SWord64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SWord64 -> SWord64 -> SWord64
    forall a. Num a => a -> a -> a
    (*)    SWord64 -> SWord64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SWord64 -> SWord64 -> SWord64
    (/!)          = CallStack
    -> String
    -> (SWord64 -> SWord64 -> SWord64)
    -> (SWord64 -> SWord64 -> (SBool, SBool))
    -> SWord64
    -> SWord64
    -> SWord64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SWord64 -> SWord64 -> SWord64
    forall a. SDivisible a => a -> a -> a
    sDiv   SWord64 -> SWord64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SWord64 -> SWord64
    negateChecked = CallStack
    -> String
    -> (SWord64 -> SWord64)
    -> (SWord64 -> (SBool, SBool))
    -> SWord64
    -> SWord64
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SWord64 -> SWord64
    forall a. Num a => a -> a
    negate SWord64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance CheckedArithmetic Int8 where
      +! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
    (+!)          = CallStack
    -> String
    -> (SInt8 -> SInt8 -> SInt8)
    -> (SInt8 -> SInt8 -> (SBool, SBool))
    -> SInt8
    -> SInt8
    -> SInt8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SInt8 -> SInt8 -> SInt8
    forall a. Num a => a -> a -> a
    (+)    SInt8 -> SInt8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
    (-!)          = CallStack
    -> String
    -> (SInt8 -> SInt8 -> SInt8)
    -> (SInt8 -> SInt8 -> (SBool, SBool))
    -> SInt8
    -> SInt8
    -> SInt8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SInt8 -> SInt8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
    (*!)          = CallStack
    -> String
    -> (SInt8 -> SInt8 -> SInt8)
    -> (SInt8 -> SInt8 -> (SBool, SBool))
    -> SInt8
    -> SInt8
    -> SInt8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SInt8 -> SInt8 -> SInt8
    forall a. Num a => a -> a -> a
    (*)    SInt8 -> SInt8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SInt8 -> SInt8 -> SInt8
    (/!)          = CallStack
    -> String
    -> (SInt8 -> SInt8 -> SInt8)
    -> (SInt8 -> SInt8 -> (SBool, SBool))
    -> SInt8
    -> SInt8
    -> SInt8
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SInt8 -> SInt8 -> SInt8
    forall a. SDivisible a => a -> a -> a
    sDiv   SInt8 -> SInt8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SInt8 -> SInt8
    negateChecked = CallStack
    -> String
    -> (SInt8 -> SInt8)
    -> (SInt8 -> (SBool, SBool))
    -> SInt8
    -> SInt8
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SInt8 -> SInt8
    forall a. Num a => a -> a
    negate SInt8 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance CheckedArithmetic Int16 where
      +! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
    (+!)          = CallStack
    -> String
    -> (SInt16 -> SInt16 -> SInt16)
    -> (SInt16 -> SInt16 -> (SBool, SBool))
    -> SInt16
    -> SInt16
    -> SInt16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SInt16 -> SInt16 -> SInt16
    forall a. Num a => a -> a -> a
    (+)    SInt16 -> SInt16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
    (-!)          = CallStack
    -> String
    -> (SInt16 -> SInt16 -> SInt16)
    -> (SInt16 -> SInt16 -> (SBool, SBool))
    -> SInt16
    -> SInt16
    -> SInt16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SInt16 -> SInt16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
    (*!)          = CallStack
    -> String
    -> (SInt16 -> SInt16 -> SInt16)
    -> (SInt16 -> SInt16 -> (SBool, SBool))
    -> SInt16
    -> SInt16
    -> SInt16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SInt16 -> SInt16 -> SInt16
    forall a. Num a => a -> a -> a
    (*)    SInt16 -> SInt16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SInt16 -> SInt16 -> SInt16
    (/!)          = CallStack
    -> String
    -> (SInt16 -> SInt16 -> SInt16)
    -> (SInt16 -> SInt16 -> (SBool, SBool))
    -> SInt16
    -> SInt16
    -> SInt16
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SInt16 -> SInt16 -> SInt16
    forall a. SDivisible a => a -> a -> a
    sDiv   SInt16 -> SInt16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SInt16 -> SInt16
    negateChecked = CallStack
    -> String
    -> (SInt16 -> SInt16)
    -> (SInt16 -> (SBool, SBool))
    -> SInt16
    -> SInt16
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SInt16 -> SInt16
    forall a. Num a => a -> a
    negate SInt16 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance CheckedArithmetic Int32 where
      +! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
    (+!)          = CallStack
    -> String
    -> (SInt32 -> SInt32 -> SInt32)
    -> (SInt32 -> SInt32 -> (SBool, SBool))
    -> SInt32
    -> SInt32
    -> SInt32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SInt32 -> SInt32 -> SInt32
    forall a. Num a => a -> a -> a
    (+)    SInt32 -> SInt32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
    (-!)          = CallStack
    -> String
    -> (SInt32 -> SInt32 -> SInt32)
    -> (SInt32 -> SInt32 -> (SBool, SBool))
    -> SInt32
    -> SInt32
    -> SInt32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SInt32 -> SInt32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
    (*!)          = CallStack
    -> String
    -> (SInt32 -> SInt32 -> SInt32)
    -> (SInt32 -> SInt32 -> (SBool, SBool))
    -> SInt32
    -> SInt32
    -> SInt32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SInt32 -> SInt32 -> SInt32
    forall a. Num a => a -> a -> a
    (*)    SInt32 -> SInt32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SInt32 -> SInt32 -> SInt32
    (/!)          = CallStack
    -> String
    -> (SInt32 -> SInt32 -> SInt32)
    -> (SInt32 -> SInt32 -> (SBool, SBool))
    -> SInt32
    -> SInt32
    -> SInt32
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SInt32 -> SInt32 -> SInt32
    forall a. SDivisible a => a -> a -> a
    sDiv   SInt32 -> SInt32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SInt32 -> SInt32
    negateChecked = CallStack
    -> String
    -> (SInt32 -> SInt32)
    -> (SInt32 -> (SBool, SBool))
    -> SInt32
    -> SInt32
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SInt32 -> SInt32
    forall a. Num a => a -> a
    negate SInt32 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance CheckedArithmetic Int64 where
      +! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
    (+!)          = CallStack
    -> String
    -> (SInt64 -> SInt64 -> SInt64)
    -> (SInt64 -> SInt64 -> (SBool, SBool))
    -> SInt64
    -> SInt64
    -> SInt64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SInt64 -> SInt64 -> SInt64
    forall a. Num a => a -> a -> a
    (+)    SInt64 -> SInt64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
    (-!)          = CallStack
    -> String
    -> (SInt64 -> SInt64 -> SInt64)
    -> (SInt64 -> SInt64 -> (SBool, SBool))
    -> SInt64
    -> SInt64
    -> SInt64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SInt64 -> SInt64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
    (*!)          = CallStack
    -> String
    -> (SInt64 -> SInt64 -> SInt64)
    -> (SInt64 -> SInt64 -> (SBool, SBool))
    -> SInt64
    -> SInt64
    -> SInt64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SInt64 -> SInt64 -> SInt64
    forall a. Num a => a -> a -> a
    (*)    SInt64 -> SInt64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SInt64 -> SInt64 -> SInt64
    (/!)          = CallStack
    -> String
    -> (SInt64 -> SInt64 -> SInt64)
    -> (SInt64 -> SInt64 -> (SBool, SBool))
    -> SInt64
    -> SInt64
    -> SInt64
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SInt64 -> SInt64 -> SInt64
    forall a. SDivisible a => a -> a -> a
    sDiv   SInt64 -> SInt64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SInt64 -> SInt64
    negateChecked = CallStack
    -> String
    -> (SInt64 -> SInt64)
    -> (SInt64 -> (SBool, SBool))
    -> SInt64
    -> SInt64
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SInt64 -> SInt64
    forall a. Num a => a -> a
    negate SInt64 -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance (KnownNat n, BVIsNonZero n) => CheckedArithmetic (WordN n) where
      +! :: (?loc::CallStack) =>
    SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    (+!)          = CallStack
    -> String
    -> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
    -> (SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool))
    -> SBV (WordN n)
    -> SBV (WordN n)
    -> SBV (WordN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    forall a. Num a => a -> a -> a
    (+)    SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) =>
    SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    (-!)          = CallStack
    -> String
    -> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
    -> (SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool))
    -> SBV (WordN n)
    -> SBV (WordN n)
    -> SBV (WordN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) =>
    SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    (*!)          = CallStack
    -> String
    -> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
    -> (SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool))
    -> SBV (WordN n)
    -> SBV (WordN n)
    -> SBV (WordN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    forall a. Num a => a -> a -> a
    (*)    SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) =>
    SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    (/!)          = CallStack
    -> String
    -> (SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n))
    -> (SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool))
    -> SBV (WordN n)
    -> SBV (WordN n)
    -> SBV (WordN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
    forall a. SDivisible a => a -> a -> a
    sDiv   SBV (WordN n) -> SBV (WordN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SBV (WordN n) -> SBV (WordN n)
    negateChecked = CallStack
    -> String
    -> (SBV (WordN n) -> SBV (WordN n))
    -> (SBV (WordN n) -> (SBool, SBool))
    -> SBV (WordN n)
    -> SBV (WordN n)
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SBV (WordN n) -> SBV (WordN n)
    forall a. Num a => a -> a
    negate SBV (WordN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    instance (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) where
      +! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    (+!)          = CallStack
    -> String
    -> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
    -> (SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool))
    -> SBV (IntN n)
    -> SBV (IntN n)
    -> SBV (IntN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "addition"       SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    forall a. Num a => a -> a -> a
    (+)    SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvAddO
      -! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    (-!)          = CallStack
    -> String
    -> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
    -> (SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool))
    -> SBV (IntN n)
    -> SBV (IntN n)
    -> SBV (IntN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "subtraction"    (-)    SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvSubO
      *! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    (*!)          = CallStack
    -> String
    -> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
    -> (SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool))
    -> SBV (IntN n)
    -> SBV (IntN n)
    -> SBV (IntN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "multiplication" SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    forall a. Num a => a -> a -> a
    (*)    SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvMulO
      /! :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    (/!)          = CallStack
    -> String
    -> (SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n))
    -> (SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool))
    -> SBV (IntN n)
    -> SBV (IntN n)
    -> SBV (IntN n)
    forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 ?loc::CallStack
    CallStack
    ?loc String
    "division"       SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
    forall a. SDivisible a => a -> a -> a
    sDiv   SBV (IntN n) -> SBV (IntN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> a -> (SBool, SBool)
    bvDivO
      negateChecked :: (?loc::CallStack) => SBV (IntN n) -> SBV (IntN n)
    negateChecked = CallStack
    -> String
    -> (SBV (IntN n) -> SBV (IntN n))
    -> (SBV (IntN n) -> (SBool, SBool))
    -> SBV (IntN n)
    -> SBV (IntN n)
    forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 ?loc::CallStack
    CallStack
    ?loc String
    "unary negation" SBV (IntN n) -> SBV (IntN n)
    forall a. Num a => a -> a
    negate SBV (IntN n) -> (SBool, SBool)
    forall a. ArithOverflow a => a -> (SBool, SBool)
    bvNegO

    -- | Zero-extend to given bits
    zx :: Int -> SVal -> SVal
    zx :: Int -> SVal -> SVal
    zx Int
    n SVal
    a
     | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    sa = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV: Unexpected zero extension: from: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    a) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " to: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
     | Bool
    True   = SVal
    p SVal -> SVal -> SVal
    `svJoin` SVal
    a
     where sa :: Int
    sa = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    a
           s :: Bool
    s  = SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    a
           p :: SVal
    p  = Kind -> Integer -> SVal
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    s (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    sa)) Integer
    0

    -- | Sign-extend to given bits. Note that we keep the signedness of the argument.
    sx :: Int -> SVal -> SVal
    sx :: Int -> SVal -> SVal
    sx Int
    n SVal
    a
     | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    sa = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV: Unexpected sign extension: from: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    a) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " to: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
     | Bool
    True   = SVal
    p SVal -> SVal -> SVal
    `svJoin` SVal
    a
     where sa :: Int
    sa = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    a
           mk :: Integer -> SVal
    mk = Kind -> Integer -> SVal
    svInteger (Kind -> Integer -> SVal) -> Kind -> Integer -> SVal
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Kind
    KBounded (SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    a) (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    sa)
           p :: SVal
    p  = SVal -> SVal -> SVal -> SVal
    svIte (SVal -> SVal
    pos SVal
    a) (Integer -> SVal
    mk Integer
    0) (Integer -> SVal
    mk (-Integer
    1))

    -- | Get the sign-bit
    signBit :: SVal -> SVal
    signBit :: SVal -> SVal
    signBit SVal
    x = SVal
    x SVal -> Int -> SVal
    `svTestBit` (SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)

    -- | Is the sign-bit high?
    neg :: SVal -> SVal
    neg :: SVal -> SVal
    neg SVal
    x = SVal -> SVal
    signBit SVal
    x SVal -> SVal -> SVal
    `svEqual` SVal
    svTrue

    -- | Is the sign-bit low?
    pos :: SVal -> SVal
    pos :: SVal -> SVal
    pos SVal
    x = SVal -> SVal
    signBit SVal
    x SVal -> SVal -> SVal
    `svEqual` SVal
    svFalse

    -- | Do these have the same sign?
    sameSign :: SVal -> SVal -> SVal
    sameSign :: SVal -> SVal -> SVal
    sameSign SVal
    x SVal
    y = (SVal -> SVal
    pos SVal
    x SVal -> SVal -> SVal
    `svAnd` SVal -> SVal
    pos SVal
    y) SVal -> SVal -> SVal
    `svOr` (SVal -> SVal
    neg SVal
    x SVal -> SVal -> SVal
    `svAnd` SVal -> SVal
    neg SVal
    y)

    -- | Do these have opposing signs?
    diffSign :: SVal -> SVal -> SVal
    diffSign :: SVal -> SVal -> SVal
    diffSign SVal
    x SVal
    y = SVal -> SVal
    svNot (SVal -> SVal -> SVal
    sameSign SVal
    x SVal
    y)

    -- | Check all true
    svAll :: [SVal] -> SVal
    svAll :: [SVal] -> SVal
    svAll = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SVal -> SVal -> SVal
    svAnd SVal
    svTrue

    -- | Are all the bits between a b (inclusive) zero?
    allZero :: Int -> Int -> SBV a -> SVal
    allZero :: forall a. Int -> Int -> SBV a -> SVal
    allZero Int
    m Int
    n (SBV SVal
    x)
      | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    sz Bool -> Bool -> Bool
    || Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0 Bool -> Bool -> Bool
    || Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n
      = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.Tools.Overflow.allZero: Received unexpected parameters: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int, Int) -> String
    forall a. Show a => a -> String
    show (Int
    m, Int
    n, Int
    sz)
      | Bool
    True
      = [SVal] -> SVal
    svAll [SVal -> Int -> SVal
    svTestBit SVal
    x Int
    i SVal -> SVal -> SVal
    `svEqual` SVal
    svFalse | Int
    i <- [Int
    m, Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1 .. Int
    n]]
      where sz :: Int
    sz = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x

    -- | Are all the bits between a b (inclusive) one?
    allOne :: Int -> Int -> SBV a -> SVal
    allOne :: forall a. Int -> Int -> SBV a -> SVal
    allOne Int
    m Int
    n (SBV SVal
    x)
      | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    sz Bool -> Bool -> Bool
    || Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0 Bool -> Bool -> Bool
    || Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n
      = String -> SVal
    forall a. HasCallStack => String -> a
    error (String -> SVal) -> String -> SVal
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.Tools.Overflow.allOne: Received unexpected parameters: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int, Int) -> String
    forall a. Show a => a -> String
    show (Int
    m, Int
    n, Int
    sz)
      | Bool
    True
      = [SVal] -> SVal
    svAll [SVal -> Int -> SVal
    svTestBit SVal
    x Int
    i SVal -> SVal -> SVal
    `svEqual` SVal
    svTrue | Int
    i <- [Int
    m, Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1 .. Int
    n]]
      where sz :: Int
    sz = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    x

    -- | Unsigned addition. Can only overflow.
    bvuaddo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvuaddo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvuaddo Int
    n SVal
    x SVal
    y = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal
    svFalse

            n' :: Int
    n'       = Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1
            overflow :: SVal
    overflow = SVal -> SVal
    neg (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> SVal -> SVal
    zx Int
    n' SVal
    x SVal -> SVal -> SVal
    `svPlus` Int -> SVal -> SVal
    zx Int
    n' SVal
    y

    -- | Signed addition.
    bvsaddo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsaddo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsaddo Int
    _n SVal
    x SVal
    y = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = [SVal] -> SVal
    svAll [SVal -> SVal
    neg SVal
    x, SVal -> SVal
    neg SVal
    y, SVal -> SVal
    pos (SVal
    x SVal -> SVal -> SVal
    `svPlus` SVal
    y)]
            overflow :: SVal
    overflow  = [SVal] -> SVal
    svAll [SVal -> SVal
    pos SVal
    x, SVal -> SVal
    pos SVal
    y, SVal -> SVal
    neg (SVal
    x SVal -> SVal -> SVal
    `svPlus` SVal
    y)]

    -- | Unsigned subtraction. Can only underflow.
    bvusubo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvusubo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvusubo Int
    _n SVal
    x SVal
    y = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal
    y SVal -> SVal -> SVal
    `svGreaterThan` SVal
    x
            overflow :: SVal
    overflow  = SVal
    svFalse

    -- | Signed subtraction.
    bvssubo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvssubo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvssubo Int
    _n SVal
    x SVal
    y = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = [SVal] -> SVal
    svAll [SVal -> SVal
    neg SVal
    x, SVal -> SVal
    pos SVal
    y, SVal -> SVal
    pos (SVal
    x SVal -> SVal -> SVal
    `svMinus` SVal
    y)]
            overflow :: SVal
    overflow  = [SVal] -> SVal
    svAll [SVal -> SVal
    pos SVal
    x, SVal -> SVal
    neg SVal
    y, SVal -> SVal
    neg (SVal
    x SVal -> SVal -> SVal
    `svMinus` SVal
    y)]

    -- | Unsigned multiplication. Can only overflow.
    bvumulo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvumulo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvumulo Int
    0 SVal
    _ SVal
    _ = (SVal
    svFalse,   SVal
    svFalse)
    bvumulo Int
    n SVal
    x SVal
    y = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal
    svFalse

            n1 :: Int
    n1        = Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1
            overflow1 :: SVal
    overflow1 = SVal -> SVal
    signBit (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> SVal -> SVal
    zx Int
    n1 SVal
    x SVal -> SVal -> SVal
    `svTimes` Int -> SVal -> SVal
    zx Int
    n1 SVal
    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 :: SVal
    overflow2 = Int -> SVal -> SVal -> SVal
    go Int
    1 SVal
    svFalse SVal
    svFalse
              where go :: Int -> SVal -> SVal -> SVal
    go Int
    i SVal
    ovf SVal
    v
                     | Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n = SVal
    v
                     | Bool
    True   = Int -> SVal -> SVal -> SVal
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) SVal
    ovf' SVal
    v'
                     where ovf' :: SVal
    ovf' = SVal
    ovf  SVal -> SVal -> SVal
    `svOr`  (SVal
    x SVal -> Int -> SVal
    `svTestBit` (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    i))
                           tmp :: SVal
    tmp  = SVal
    ovf' SVal -> SVal -> SVal
    `svAnd` (SVal
    y SVal -> Int -> SVal
    `svTestBit` Int
    i)
                           v' :: SVal
    v'   = SVal
    tmp SVal -> SVal -> SVal
    `svOr` SVal
    v

            overflow :: SVal
    overflow = SVal
    overflow1 SVal -> SVal -> SVal
    `svOr` SVal
    overflow2

    -- | Signed multiplication.
    bvsmulo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsmulo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsmulo Int
    0 SVal
    _ SVal
    _ = (SVal
    svFalse,   SVal
    svFalse)
    bvsmulo Int
    n SVal
    x SVal
    y = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal -> SVal -> SVal
    diffSign SVal
    x SVal
    y SVal -> SVal -> SVal
    `svAnd` SVal
    overflowPossible
            overflow :: SVal
    overflow  = SVal -> SVal -> SVal
    sameSign SVal
    x SVal
    y SVal -> SVal -> SVal
    `svAnd` SVal
    overflowPossible

            n1 :: Int
    n1        = Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1
            overflow1 :: SVal
    overflow1 = (SVal
    xy1 SVal -> Int -> SVal
    `svTestBit` Int
    n) SVal -> SVal -> SVal
    `svXOr` (SVal
    xy1 SVal -> Int -> SVal
    `svTestBit` (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))
               where xy1 :: SVal
    xy1 = Int -> SVal -> SVal
    sx Int
    n1 SVal
    x SVal -> SVal -> SVal
    `svTimes` Int -> SVal -> SVal
    sx Int
    n1 SVal
    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 :: SVal
    overflow2 = Int -> SVal -> SVal -> SVal
    go Int
    1 SVal
    svFalse SVal
    svFalse
               where sY :: SVal
    sY = SVal -> SVal
    signBit SVal
    y
                     sX :: SVal
    sX = SVal -> SVal
    signBit SVal
    x
                     go :: Int -> SVal -> SVal -> SVal
    go Int
    i SVal
    v SVal
    a_acc
                      | Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n = SVal
    v
                      | Bool
    True       = Int -> SVal -> SVal -> SVal
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) SVal
    v' SVal
    a_acc'
                      where b :: SVal
    b      = SVal
    sY SVal -> SVal -> SVal
    `svXOr` (SVal
    y SVal -> Int -> SVal
    `svTestBit` Int
    i)
                            a :: SVal
    a      = SVal
    sX SVal -> SVal -> SVal
    `svXOr` (SVal
    x SVal -> Int -> SVal
    `svTestBit` (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    i))
                            a_acc' :: SVal
    a_acc' = SVal
    a SVal -> SVal -> SVal
    `svOr` SVal
    a_acc
                            tmp :: SVal
    tmp    = SVal
    a_acc' SVal -> SVal -> SVal
    `svAnd` SVal
    b
                            v' :: SVal
    v'     = SVal
    tmp SVal -> SVal -> SVal
    `svOr` SVal
    v

            overflowPossible :: SVal
    overflowPossible = SVal
    overflow1 SVal -> SVal -> SVal
    `svOr` SVal
    overflow2

    -- | Is this a concrete value?
    known :: SVal -> Bool
    known :: SVal -> Bool
    known (SVal Kind
    _ (Left CV
    _)) = Bool
    True
    known SVal
    _                 = Bool
    False

    -- | Unsigned multiplication, fast version using z3 primitives.
    bvumuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
    bvumuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
    bvumuloFast Int
    n SVal
    x SVal
    y
       | SVal -> Bool
    known SVal
    x Bool -> Bool -> Bool
    && SVal -> Bool
    known SVal
    y                         -- Not particularly fast, but avoids shipping of to the solver
       = Int -> SVal -> SVal -> (SVal, SVal)
    bvumulo Int
    n SVal
    x SVal
    y
       | Bool
    True
       = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = (SVal, SVal) -> SVal
    forall a b. (a, b) -> a
    fst ((SVal, SVal) -> SVal) -> (SVal, SVal) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> SVal -> SVal -> (SVal, SVal)
    bvumulo Int
    n SVal
    x SVal
    y         -- No internal version for underflow exists (because it can't underflow)
            overflow :: SVal
    overflow  = OvOp -> SVal -> SVal -> SVal
    svMkOverflow OvOp
    Overflow_UMul_OVFL SVal
    x SVal
    y

    -- | Signed multiplication, fast version using z3 primitives.
    bvsmuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsmuloFast :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsmuloFast Int
    n SVal
    x SVal
    y
      | SVal -> Bool
    known SVal
    x Bool -> Bool -> Bool
    && SVal -> Bool
    known SVal
    y                -- Not particularly fast, but avoids shipping of to the solver
      = Int -> SVal -> SVal -> (SVal, SVal)
    bvsmulo Int
    n SVal
    x SVal
    y
      | Bool
    True
      = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = OvOp -> SVal -> SVal -> SVal
    svMkOverflow OvOp
    Overflow_SMul_UDFL SVal
    x SVal
    y
            overflow :: SVal
    overflow  = OvOp -> SVal -> SVal -> SVal
    svMkOverflow OvOp
    Overflow_SMul_OVFL SVal
    x SVal
    y

    -- | Unsigned division. Neither underflows, nor overflows.
    bvudivo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvudivo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvudivo Int
    _ SVal
    _ SVal
    _ = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal
    svFalse
            overflow :: SVal
    overflow  = SVal
    svFalse

    -- | Signed division. Can only overflow.
    bvsdivo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsdivo :: Int -> SVal -> SVal -> (SVal, SVal)
    bvsdivo Int
    n SVal
    x SVal
    y = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal
    svFalse

            ones :: SVal
    ones      = Kind -> Integer -> SVal
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    True Int
    n) (-Integer
    1)
            topSet :: SVal
    topSet    = Kind -> Integer -> SVal
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    True Int
    n) (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))

            overflow :: SVal
    overflow = [SVal] -> SVal
    svAll [SVal
    x SVal -> SVal -> SVal
    `svEqual` SVal
    topSet, SVal
    y SVal -> SVal -> SVal
    `svEqual` SVal
    ones]

    -- | Unsigned negation. Neither underflows, nor overflows.
    bvunego :: Int -> SVal -> (SVal, SVal)
    bvunego :: Int -> SVal -> (SVal, SVal)
    bvunego Int
    _ SVal
    _ = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal
    svFalse
            overflow :: SVal
    overflow  = SVal
    svFalse

    -- | Signed negation. Can only overflow.
    bvsnego :: Int -> SVal -> (SVal, SVal)
    bvsnego :: Int -> SVal -> (SVal, SVal)
    bvsnego Int
    n SVal
    x = (SVal
    underflow, SVal
    overflow)
      where underflow :: SVal
    underflow = SVal
    svFalse

            topSet :: SVal
    topSet    = Kind -> Integer -> SVal
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    True Int
    n) (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1))
            overflow :: SVal
    overflow  = SVal
    x SVal -> SVal -> SVal
    `svEqual` SVal
    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, (sFalse, sFalse))
    -- 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, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> (SBV b, (SBool, SBool))
    sFromIntegralO :: forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> (SBV b, (SBool, SBool))
    sFromIntegralO SBV a
    x = case (SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    x, Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b)) of
                         (KBounded Bool
    False Int
    n, KBounded Bool
    False Int
    m) -> (SBV b
    res, Int -> Int -> (SBool, SBool)
    u2u Int
    n Int
    m)
                         (KBounded Bool
    False Int
    n, KBounded Bool
    True  Int
    m) -> (SBV b
    res, Int -> Int -> (SBool, SBool)
    u2s Int
    n Int
    m)
                         (KBounded Bool
    True Int
    n,  KBounded Bool
    False Int
    m) -> (SBV b
    res, Int -> Int -> (SBool, SBool)
    s2u Int
    n Int
    m)
                         (KBounded Bool
    True Int
    n,  KBounded Bool
    True  Int
    m) -> (SBV b
    res, Int -> Int -> (SBool, SBool)
    s2s Int
    n Int
    m)
                         (Kind
    KUnbounded,       KBounded Bool
    s Int
    m)     -> (SBV b
    res, Bool -> Int -> (SBool, SBool)
    checkBounds Bool
    s Int
    m)
                         (KBounded{},       Kind
    KUnbounded)       -> (SBV b
    res, (SBool
    sFalse, SBool
    sFalse))
                         (Kind
    KUnbounded,       Kind
    KUnbounded)       -> (SBV b
    res, (SBool
    sFalse, SBool
    sFalse))
                         (Kind
    kFrom,            Kind
    kTo)              -> String -> (SBV b, (SBool, SBool))
    forall a. HasCallStack => String -> a
    error (String -> (SBV b, (SBool, SBool)))
    -> String -> (SBV b, (SBool, SBool))
    forall a b. (a -> b) -> a -> b
    $ String
    "sFromIntegralO: Expected bounded-BV types, received: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    kFrom, Kind
    kTo)

      where res :: SBV b
            res :: SBV b
    res = SBV a -> SBV b
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV a
    x

            checkBounds :: Bool -> Int -> (SBool, SBool)
            checkBounds :: Bool -> Int -> (SBool, SBool)
    checkBounds Bool
    signed Int
    sz = (SInteger
    ix SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    lb, SInteger
    ix SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .> Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    ub)
              where ix :: SInteger
                    ix :: SInteger
    ix = SBV a -> SInteger
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV a
    x

                    s :: Integer
                    s :: Integer
    s = Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    sz

                    ub :: Integer
                    ub :: Integer
    ub | Bool
    signed = Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Integer
    s Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1
                       | Bool
    True   = Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    s       Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1

                    lb :: Integer
                    lb :: Integer
    lb | Bool
    signed = -Integer
    ubInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1
                       | Bool
    True   = Integer
    0

            u2u :: Int -> Int -> (SBool, SBool)
            u2u :: Int -> Int -> (SBool, SBool)
    u2u Int
    n Int
    m = (SBool
    underflow, SBool
    overflow)
              where underflow :: SBool
    underflow  = SBool
    sFalse
                    overflow :: SBool
    overflow
                      | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    m = SBool
    sFalse
                      | Bool
    True   = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal
    svNot (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> SBV a -> SVal
    forall a. Int -> Int -> SBV a -> SVal
    allZero (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Int
    m SBV a
    x

            u2s :: Int -> Int -> (SBool, SBool)
            u2s :: Int -> Int -> (SBool, SBool)
    u2s Int
    n Int
    m = (SBool
    underflow, SBool
    overflow)
              where underflow :: SBool
    underflow = SBool
    sFalse
                    overflow :: SBool
    overflow
                      | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    n = SBool
    sFalse
                      | Bool
    True  = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ SVal -> SVal
    svNot (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> SBV a -> SVal
    forall a. Int -> Int -> SBV a -> SVal
    allZero (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) SBV a
    x

            s2u :: Int -> Int -> (SBool, SBool)
            s2u :: Int -> Int -> (SBool, SBool)
    s2u Int
    n Int
    m = (SBool
    forall {a}. SBV a
    underflow, SBool
    overflow)
              where underflow :: SBV a
    underflow = SVal -> SBV a
    forall a. SVal -> SBV a
    SBV (SVal -> SBV a) -> SVal -> SBV a
    forall a b. (a -> b) -> a -> b
    $ (SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV SBV a
    x SVal -> Int -> SVal
    `svTestBit` (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)) SVal -> SVal -> SVal
    `svEqual` SVal
    svTrue

                    overflow :: SBool
    overflow
                      | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 = SBool
    sFalse
                      | Bool
    True       = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ [SVal] -> SVal
    svAll [(SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV SBV a
    x SVal -> Int -> SVal
    `svTestBit` (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)) SVal -> SVal -> SVal
    `svEqual` SVal
    svFalse, SVal -> SVal
    svNot (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> SBV a -> SVal
    forall a. Int -> Int -> SBV a -> SVal
    allZero (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Int
    m SBV a
    x]

            s2s :: Int -> Int -> (SBool, SBool)
            s2s :: Int -> Int -> (SBool, SBool)
    s2s Int
    n Int
    m = (SBool
    underflow, SBool
    overflow)
              where underflow :: SBool
    underflow
                      | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    n = SBool
    sFalse
                      | Bool
    True  = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ [SVal] -> SVal
    svAll [(SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV SBV a
    x SVal -> Int -> SVal
    `svTestBit` (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)) SVal -> SVal -> SVal
    `svEqual` SVal
    svTrue,  SVal -> SVal
    svNot (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> SBV a -> SVal
    forall a. Int -> Int -> SBV a -> SVal
    allOne  (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) SBV a
    x]

                    overflow :: SBool
    overflow
                      | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    n = SBool
    sFalse
                      | Bool
    True  = SVal -> SBool
    forall a. SVal -> SBV a
    SBV (SVal -> SBool) -> SVal -> SBool
    forall a b. (a -> b) -> a -> b
    $ [SVal] -> SVal
    svAll [(SBV a -> SVal
    forall a. SBV a -> SVal
    unSBV SBV a
    x SVal -> Int -> SVal
    `svTestBit` (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)) SVal -> SVal -> SVal
    `svEqual` SVal
    svFalse, SVal -> SVal
    svNot (SVal -> SVal) -> SVal -> SVal
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> SBV a -> SVal
    forall a. Int -> Int -> SBV a -> SVal
    allZero (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) SBV a
    x]

    -- | Version of 'sFromIntegral' that has calls to 'Data.SBV.sAssert' for checking no overflow/underflow can happen. Use it with a 'Data.SBV.safe' call.
    sFromIntegralChecked :: forall a b. (?loc :: CallStack, Integral a, HasKind a, HasKind b, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
    sFromIntegralChecked :: forall a b.
    (?loc::CallStack, Integral a, HasKind a, HasKind b, Num a,
     SymVal a, HasKind b, Num b, SymVal b) =>
    SBV a -> SBV b
    sFromIntegralChecked SBV a
    x = Maybe CallStack -> String -> SBool -> SBV b -> SBV b
    forall a.
    HasKind a =>
    Maybe CallStack -> String -> SBool -> SBV a -> SBV a
    sAssert (CallStack -> Maybe CallStack
    forall a. a -> Maybe a
    Just ?loc::CallStack
    CallStack
    ?loc) (String -> String
    msg String
    "underflows") (SBool -> SBool
    sNot SBool
    u)
                           (SBV b -> SBV b) -> SBV b -> SBV b
    forall a b. (a -> b) -> a -> b
    $ Maybe CallStack -> String -> SBool -> SBV b -> SBV b
    forall a.
    HasKind a =>
    Maybe CallStack -> String -> SBool -> SBV a -> SBV a
    sAssert (CallStack -> Maybe CallStack
    forall a. a -> Maybe a
    Just ?loc::CallStack
    CallStack
    ?loc) (String -> String
    msg String
    "overflows")  (SBool -> SBool
    sNot SBool
    o)
                             SBV b
    r
      where kFrom :: String
    kFrom = Kind -> String
    forall a. Show a => a -> String
    show (Kind -> String) -> Kind -> String
    forall a b. (a -> b) -> a -> b
    $ SBV a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBV a
    x
            kTo :: String
    kTo   = Kind -> String
    forall a. Show a => a -> String
    show (Kind -> String) -> Kind -> String
    forall a b. (a -> b) -> a -> b
    $ Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b)
            msg :: String -> String
    msg String
    c = String
    "Casting from " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    kFrom String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    kTo String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c

            (SBV b
    r, (SBool
    u, SBool
    o)) = SBV a -> (SBV b, (SBool, SBool))
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> (SBV b, (SBool, SBool))
    sFromIntegralO SBV a
    x

    -- Helpers
    l2 :: (SVal -> SVal -> (SBool, SBool)) -> SBV a -> SBV a -> (SBool, SBool)
    l2 :: forall a.
    (SVal -> SVal -> (SBool, SBool))
    -> SBV a -> SBV a -> (SBool, SBool)
    l2 SVal -> SVal -> (SBool, SBool)
    f (SBV SVal
    a) (SBV SVal
    b) = SVal -> SVal -> (SBool, SBool)
    f SVal
    a SVal
    b

    l1 :: (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 :: forall a. (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)
    l1 SVal -> (SBool, SBool)
    f (SBV SVal
    a) = SVal -> (SBool, SBool)
    f SVal
    a

    signPick2 :: (Int -> SVal -> SVal -> (SVal, SVal)) -> (Int -> SVal -> SVal -> (SVal, SVal)) -> (SVal -> SVal -> (SBool, SBool))
    signPick2 :: (Int -> SVal -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> SVal -> (SVal, SVal))
    -> SVal
    -> SVal
    -> (SBool, SBool)
    signPick2 Int -> SVal -> SVal -> (SVal, SVal)
    fu Int -> SVal -> SVal -> (SVal, SVal)
    fs SVal
    a SVal
    b
     | SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    a = let (SVal
    u, SVal
    o) = Int -> SVal -> SVal -> (SVal, SVal)
    fs Int
    n SVal
    a SVal
    b in (SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    u, SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    o)
     | Bool
    True      = let (SVal
    u, SVal
    o) = Int -> SVal -> SVal -> (SVal, SVal)
    fu Int
    n SVal
    a SVal
    b in (SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    u, SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    o)
     where n :: Int
    n = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    a

    signPick1 :: (Int -> SVal -> (SVal, SVal)) -> (Int -> SVal -> (SVal, SVal)) -> (SVal -> (SBool, SBool))
    signPick1 :: (Int -> SVal -> (SVal, SVal))
    -> (Int -> SVal -> (SVal, SVal)) -> SVal -> (SBool, SBool)
    signPick1 Int -> SVal -> (SVal, SVal)
    fu Int -> SVal -> (SVal, SVal)
    fs SVal
    a
     | SVal -> Bool
    forall a. HasKind a => a -> Bool
    hasSign SVal
    a = let (SVal
    u, SVal
    o) = Int -> SVal -> (SVal, SVal)
    fs Int
    n SVal
    a in (SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    u, SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    o)
     | Bool
    True      = let (SVal
    u, SVal
    o) = Int -> SVal -> (SVal, SVal)
    fu Int
    n SVal
    a in (SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    u, SVal -> SBool
    forall a. SVal -> SBV a
    SBV SVal
    o)
     where n :: Int
    n = SVal -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SVal
    a

    checkOp1 :: (HasKind a, HasKind b) => CallStack -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 :: forall a b.
    (HasKind a, HasKind b) =>
    CallStack
    -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b
    checkOp1 CallStack
    loc String
    w a -> SBV b
    op a -> (SBool, SBool)
    cop a
    a = Maybe CallStack -> String -> SBool -> SBV b -> SBV b
    forall a.
    HasKind a =>
    Maybe CallStack -> String -> SBool -> SBV a -> SBV a
    sAssert (CallStack -> Maybe CallStack
    forall a. a -> Maybe a
    Just CallStack
    loc) (String -> String
    msg String
    "underflows") (SBool -> SBool
    sNot SBool
    u)
                            (SBV b -> SBV b) -> SBV b -> SBV b
    forall a b. (a -> b) -> a -> b
    $ Maybe CallStack -> String -> SBool -> SBV b -> SBV b
    forall a.
    HasKind a =>
    Maybe CallStack -> String -> SBool -> SBV a -> SBV a
    sAssert (CallStack -> Maybe CallStack
    forall a. a -> Maybe a
    Just CallStack
    loc) (String -> String
    msg String
    "overflows")  (SBool -> SBool
    sNot SBool
    o)
                            (SBV b -> SBV b) -> SBV b -> SBV b
    forall a b. (a -> b) -> a -> b
    $ a -> SBV b
    op a
    a
      where k :: String
    k = Kind -> String
    forall a. Show a => a -> String
    show (Kind -> String) -> Kind -> String
    forall a b. (a -> b) -> a -> b
    $ a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    a
            msg :: String -> String
    msg String
    c = String
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c

            (SBool
    u, SBool
    o) = a -> (SBool, SBool)
    cop a
    a

    checkOp2 :: (HasKind a, HasKind c) => CallStack -> String -> (a -> b -> SBV c) -> (a -> b -> (SBool, SBool)) -> a -> b -> SBV c
    checkOp2 :: forall a c b.
    (HasKind a, HasKind c) =>
    CallStack
    -> String
    -> (a -> b -> SBV c)
    -> (a -> b -> (SBool, SBool))
    -> a
    -> b
    -> SBV c
    checkOp2 CallStack
    loc String
    w a -> b -> SBV c
    op a -> b -> (SBool, SBool)
    cop a
    a b
    b = Maybe CallStack -> String -> SBool -> SBV c -> SBV c
    forall a.
    HasKind a =>
    Maybe CallStack -> String -> SBool -> SBV a -> SBV a
    sAssert (CallStack -> Maybe CallStack
    forall a. a -> Maybe a
    Just CallStack
    loc) (String -> String
    msg String
    "underflows") (SBool -> SBool
    sNot SBool
    u)
                              (SBV c -> SBV c) -> SBV c -> SBV c
    forall a b. (a -> b) -> a -> b
    $ Maybe CallStack -> String -> SBool -> SBV c -> SBV c
    forall a.
    HasKind a =>
    Maybe CallStack -> String -> SBool -> SBV a -> SBV a
    sAssert (CallStack -> Maybe CallStack
    forall a. a -> Maybe a
    Just CallStack
    loc) (String -> String
    msg String
    "overflows")  (SBool -> SBool
    sNot SBool
    o)
                              (SBV c -> SBV c) -> SBV c -> SBV c
    forall a b. (a -> b) -> a -> b
    $ a
    a a -> b -> SBV c
    `op` b
    b
      where k :: String
    k = Kind -> String
    forall a. Show a => a -> String
    show (Kind -> String) -> Kind -> String
    forall a b. (a -> b) -> a -> b
    $ a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    a
            msg :: String -> String
    msg String
    c = String
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    c

            (SBool
    u, SBool
    o) = a
    a a -> b -> (SBool, SBool)
    `cop` b
    b