diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,20 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.6.0 _(2024-08-27)_
+
+### Added
+- Support for signed BitVec operations.
+- Added constructor `Rem` for `Expr t`.
+
+### Changed
+- *(breaking change)* Enhanced the type of `BvSort Nat` to `BvSort BvEnc Nat` where `BvEnc = Unsigned | Signed`.
+  Before, the API only allowed unsigned BitVec, therefore `BvSort n` now becomes `BvSort Unsigned n`.
+  The promoted type `BvEnc` is phantom and only used for differentiating instances for `Num`, ...
+- Moved `Language.Hasmtlib.Internal.Bitvec` to `Language.Hasmtlib.Type.Bitvec`, exported API with `Language.Hasmtlib`
+- Removed constructors `StrLT` and `StrLTHE` from `Expr t`.
+- Fixed wrong implementation of Num for `Bitvec`. `(+)`, `(-)` and `(*)` had invalid definitions.
+
 ## v2.5.1 _(2024-08-26)_
 
 ### Added
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -17,7 +17,7 @@
 v3Add :: V3 (Expr RealSort) -> V3 (Expr RealSort) -> V3 (Expr RealSort)
 v3Add = liftA2 (+)
 ```
-Even better, the [Expr-GADT](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Internal/Expr.hs) allows a polymorph definition:
+Even better, the [Expr-GADT](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Expr.hs) allows a polymorph definition:
 ```haskell
 v3Add :: Num (Expr t) => V3 (Expr t) -> V3 (Expr t) -> V3 (Expr t)
 v3Add = liftA2 (+)
@@ -63,26 +63,28 @@
         BoolSort
       | IntSort
       | RealSort
-      | BvSort Nat
+      | BvSort BvEnc Nat
       | ArraySort SMTSort SMTSort
       | StringSort
     data Expr (t :: SMTSort) where ...
 
     ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t
   ```
-- [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec, Array & String
-- [x] Type-level length-indexed Bitvectors for BitVec
+- [x] Full SMTLib 2.6 standard support for Sorts Bool, Int, Real, BitVec, Array & String
+- [x] Type-level length-indexed Bitvectors with type-level encoding (Signed/Unsigned) for BitVec
   ```haskell
-    bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
+  bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
+  bvLShR :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort enc n) -> Expr (BvSort Unsigned n)
+  bvAShR :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort enc n) -> Expr (BvSort Signed n)
   ```
-- [x] Pure API with Expression-instances for Num, Floating, Bounded, ...
+- [x] Pure API with plenty common instances: `Num`, `Floating`, `Bounded`, `Bits`, `Ixed` and many more
   ```haskell
     solveWith @SMT (solver yices) $ do
       setLogic "QF_BV"
-      x <- var @(BvSort 16)
-      y <- var
-      assert $ x - (maxBound `mod` 8) === y * y
-      return (x,y)
+      x <- var @(BvSort Signed 16)
+      let f = x >? 42 && (x `div` 84 === maxBound - 100)
+      assert f
+      return x
   ```
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)
   ```haskell
@@ -90,11 +92,6 @@
     type Solver s m = s -> m (Result, Solution)
   ```
 - [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla
-  ```haskell
-    (result, solution) <- solveWith @SMT (solver mathsat) $ do
-      setLogic "QF_LIA"
-      assert $ ...
-  ```
 - [x] Incremental solving
   ```haskell
       cvc5Living <- interactiveSolver cvc5
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.5.1
+version:               2.6.0
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
@@ -33,7 +33,6 @@
                      , Language.Hasmtlib.Variable
                      , Language.Hasmtlib.Counting
                      , Language.Hasmtlib.Internal.Parser
-                     , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
                      , Language.Hasmtlib.Internal.Sharing
                      , Language.Hasmtlib.Internal.Uniplate1
@@ -56,6 +55,7 @@
                      , Language.Hasmtlib.Type.Solver
                      , Language.Hasmtlib.Type.Option
                      , Language.Hasmtlib.Type.ArrayMap
+                     , Language.Hasmtlib.Type.Bitvec
 
   build-depends:       attoparsec                   >= 0.14.4 && < 1
                      , base                         >= 4.17.2 && < 5
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -11,6 +11,7 @@
   , module Language.Hasmtlib.Type.SMTSort
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
+  , module Language.Hasmtlib.Type.Bitvec
   , module Language.Hasmtlib.Boolean
   , module Language.Hasmtlib.Codec
   , module Language.Hasmtlib.Counting
@@ -37,6 +38,7 @@
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Counting
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -6,13 +6,15 @@
 module Language.Hasmtlib.Codec where
 
 import Prelude hiding (not, (&&), (||), all, and)
-import Language.Hasmtlib.Internal.Bitvec
-import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..), unwrapValue, wrapValue)
+import Language.Hasmtlib.Type.Bitvec
+import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..))
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.SMTSort
+import Language.Hasmtlib.Type.Value
 import Language.Hasmtlib.Boolean
 import Data.Kind
+import Data.Proxy
 import Data.Coerce
 import qualified Data.List as List
 import Data.Bits hiding (And, Xor, xor)
@@ -23,9 +25,9 @@
 import Data.Tree (Tree)
 import qualified Data.Text as Text
 import Data.Monoid (Sum, Product, First, Last, Dual)
-import Data.Functor.Identity (Identity)
 import qualified Data.Vector.Sized as V
 import Control.Monad
+import Control.Lens hiding (from, to)
 import GHC.Generics
 import GHC.TypeLits
 
@@ -70,7 +72,14 @@
 instance KnownSMTSort t => Codec (Expr t) where
   type Decoded (Expr t) = HaskellType t
   decode sol (Var var)  = do
-    (IntValueMap m) <- DMap.lookup (sortSing @t) sol
+    let sungSort = sortSing @t
+    (IntValueMap m) <- case sungSort of
+      SBvSort enc n -> case bvEncSing' enc of
+      -- Solution contains all BV as unsigned, if we have a Signed one we check the Unsigned ones and flip BvEnc
+        SUnsigned -> DMap.lookup sungSort sol
+        SSigned -> DMap.lookup (SBvSort (Proxy @Unsigned) n) sol <&>
+          \case (IntValueMap ubvs) -> IntValueMap $ fmap (\case (BvValue ubv) -> BvValue $ asSigned ubv) ubvs
+      _ -> DMap.lookup sungSort sol
     val <- IM.lookup (coerce var) m
     return $ unwrapValue val
   decode _ (Constant v)         = Just $ unwrapValue v
@@ -80,6 +89,7 @@
   decode sol (Mul x y)          = (*)   <$> decode sol x <*> decode sol y
   decode sol (Abs x)            = fmap abs     (decode sol x)
   decode sol (Mod x y)          = mod   <$> decode sol x <*> decode sol y
+  decode sol (Rem x y)          = rem   <$> decode sol x <*> decode sol y
   decode sol (IDiv x y)         = div   <$> decode sol x <*> decode sol y
   decode sol (Div x y)          = (/)   <$> decode sol x <*> decode sol y
   decode sol (LTH x y)          = (<)   <$> decode sol x <*> decode sol y
@@ -115,17 +125,25 @@
   decode sol (Ite p t f)        = (\p' t' f' -> if p' then t' else f') <$> decode sol p <*> decode sol t <*> decode sol f
   decode sol (BvNand x y)       = nand <$> sequenceA [decode sol x, decode sol y]
   decode sol (BvNor x y)        = nor  <$> sequenceA [decode sol x, decode sol y]
-  decode sol (BvShL x y)        = join $ bvShL <$> decode sol x <*> decode sol y
-  decode sol (BvLShR x y)       = join $ bvLShR <$> decode sol x <*> decode sol y
-  decode sol (BvConcat x y)     = bvConcat <$> decode sol x <*> decode sol y
+  decode sol (BvShL x y)        = do
+    x' <- decode sol x
+    y' <- decode sol y
+    return $ shiftL x' $ fromIntegral (toInteger y')
+  decode sol (BvLShR x y)       = do
+    x' <- decode sol x
+    y' <- decode sol y
+    return $ shiftR x' $ fromIntegral (toInteger y')
+  decode sol (BvAShR x y)       = do
+    x' <- decode sol x
+    y' <- decode sol y
+    return $ shiftR x' $ fromIntegral (toInteger y')
+  decode sol (BvConcat x y)     = bitvecConcat <$> decode sol x <*> decode sol y
   decode sol (BvRotL i x)       = rotateL <$> decode sol x <*> pure (fromIntegral i)
   decode sol (BvRotR i x)       = rotateR <$> decode sol x <*> pure (fromIntegral i)
   decode sol (ArrSelect i arr)  = arrSelect <$> decode sol i <*> decode sol arr
   decode sol (ArrStore i x arr) = arrStore <$> decode sol i <*> decode sol x <*> decode sol arr
   decode sol (StrConcat x y)         = (<>) <$> decode sol x <*> decode sol y
   decode sol (StrLength x)           = toInteger . Text.length <$> decode sol x
-  decode sol (StrLT x y)             = (<) <$> decode sol x <*> decode sol y
-  decode sol (StrLTHE x y)           = (<=) <$> decode sol x <*> decode sol y
   decode sol (StrAt x i)             = (\x' i' -> Text.singleton $ Text.index x' (fromInteger i')) <$> decode sol x <*> decode sol i
   decode sol (StrSubstring x i j)    = (\x' (fromInteger -> i') (fromInteger -> j') -> Text.take (j' - i') $ Text.drop i' x') <$> decode sol x <*> decode sol i <*> decode sol j
   decode sol (StrPrefixOf x y)       = Text.isPrefixOf <$> decode sol x <*> decode sol y
diff --git a/src/Language/Hasmtlib/Internal/Bitvec.hs b/src/Language/Hasmtlib/Internal/Bitvec.hs
deleted file mode 100644
--- a/src/Language/Hasmtlib/Internal/Bitvec.hs
+++ /dev/null
@@ -1,124 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE ViewPatterns #-}
-
-module Language.Hasmtlib.Internal.Bitvec where
-
-import Prelude hiding ((&&), (||), not)
-import Language.Hasmtlib.Boolean
-import Language.Hasmtlib.Internal.Render
-import Data.ByteString.Builder
-import Data.Bit
-import Data.Bits
-import Data.Coerce
-import Data.Finite hiding (shift)
-import Data.Proxy
-import Data.Ratio ((%))
-import Data.Bifunctor
-import qualified Data.Vector.Unboxed.Sized as V
-import GHC.TypeNats
-
--- | Unsigned and length-indexed bitvector with MSB first.
-newtype Bitvec (n :: Nat) = Bitvec { unBitvec :: V.Vector n Bit }
-  deriving newtype (Eq, Ord, Boolean)
-
-instance KnownNat n => Bits (Bitvec n) where
-  (.&.) = (&&)
-  (.|.) = (||)
-  xor = Language.Hasmtlib.Boolean.xor
-  complement = not
-  shift bv i  = coerce $ shift (coerce @_ @(V.Vector n Bit) bv) (negate i)
-  rotate bv i = coerce $ rotate (coerce @_ @(V.Vector n Bit) bv) (negate i)
-  bitSize _ = fromIntegral $ natVal (Proxy @n)
-  bitSizeMaybe _ = Just $ fromIntegral $ natVal (Proxy @n)
-  isSigned _ = false
-  testBit bv = testBit (V.reverse (coerce @_ @(V.Vector n Bit) bv))
-  bit (toInteger -> i) = coerce $ V.reverse $ V.replicate @n (Bit False) V.// [(finite i, Bit True)]
-  popCount = coerce . popCount . coerce @_ @(V.Vector n Bit)
-
-instance Show (Bitvec n) where
-  show = V.toList . V.map (\b -> if coerce b then '1' else '0') . coerce @_ @(V.Vector n Bit)
-
-instance Render (Bitvec n) where
-  render = stringUtf8 . show
-  {-# INLINEABLE render #-}
-
-instance KnownNat n => Num (Bitvec n) where
-   fromInteger x = coerce . V.reverse $ V.generate @n (coerce . testBit x . fromInteger . getFinite)
-   negate        = id
-   abs           = id
-   signum _      = 0
-   (coerce -> x) + (coerce -> y) = coerce @(V.Vector n Bit) $ x + y
-   (coerce -> x) - (coerce -> y) = coerce @(V.Vector n Bit) $ x - y
-   (coerce -> x) * (coerce -> y) = coerce @(V.Vector n Bit) $ x * y
-
-instance KnownNat n => Bounded (Bitvec n) where
-  minBound = coerce $ V.replicate @n false
-  maxBound = coerce $ V.replicate @n true
-
-instance KnownNat n => Enum (Bitvec n) where
-  succ x   = x + 1
-  pred x   = x - 1
-  toEnum   = fromInteger . toInteger
-  fromEnum = V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse . coerce @_ @(V.Vector n Bit)
-
-instance KnownNat n => Real (Bitvec n) where
-  toRational x = toInteger (fromEnum x) % 1
-
-instance KnownNat n => Integral (Bitvec n) where
-  toInteger = fromIntegral . fromEnum
-  quotRem x y = bimap fromInteger fromInteger $ quotRem (toInteger x) (toInteger y)
-
-bvReverse :: Bitvec n -> Bitvec n
-bvReverse = coerce . V.reverse . coerce
-
-bvReplicate :: forall n. KnownNat n => Bit -> Bitvec n
-bvReplicate = coerce . V.replicate @n
-
-bvReplicate' :: forall n proxy. KnownNat n => proxy n -> Bit -> Bitvec n
-bvReplicate' _ = bvReplicate
-
-bvGenerate :: forall n. KnownNat n => (Finite n -> Bit) -> Bitvec n
-bvGenerate = coerce . V.generate @n . coerce
-
-bvConcat :: Bitvec n -> Bitvec m -> Bitvec (n + m)
-bvConcat (coerce -> x) (coerce -> y) = coerce $ x V.++ y
-
-bvTake' :: forall n m proxy . KnownNat n => proxy n -> Bitvec (n+m) -> Bitvec n
-bvTake' p = coerce . V.take' p . coerce
-
-bvDrop' :: forall n m proxy . KnownNat n => proxy n -> Bitvec (n+m) -> Bitvec m
-bvDrop' p = coerce . V.drop' p . coerce
-
-bvSplitAt' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n+m) -> (Bitvec n, Bitvec m)
-bvSplitAt' p = coerce . V.splitAt' p . coerce
-
-bvToList :: Bitvec n -> [Bit]
-bvToList = V.toList . coerce
-
-bvFromListN :: forall n. KnownNat n => [Bit] -> Maybe (Bitvec n)
-bvFromListN = coerce . V.fromListN @n
-
-bvFromListN' :: forall n. KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec n)
-bvFromListN' _ = bvFromListN
-
-bvShL :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
-bvShL x y = bvFromListN $ (++ replicate i false) $ drop i $ bvToList x
-  where
-    i = fromIntegral y
-
-bvLShR :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
-bvLShR x y = fmap bvReverse $ bvFromListN $ (++ replicate i false) $ drop i $ bvToList $ bvReverse x
-  where
-    i = fromIntegral y
-
-bvZeroExtend :: KnownNat i => Proxy i -> Bitvec n -> Bitvec (n+i)
-bvZeroExtend p x = bvConcat x $ bvReplicate' p false
-
-bvExtract :: forall n i j.
-  ( KnownNat i, KnownNat ((j - i) + 1)
-  , (i+(n-i)) ~ n
-  , (((j - i) + 1) + ((n - i)-((j - i) + 1))) ~ (n - i)
-  ) => Proxy i -> Proxy j -> Bitvec n -> Bitvec (( j - i ) + 1)
-bvExtract pri _ x = bvTake' @_ @((n-i)-((j-i)+1)) (Proxy @((j-i)+1)) x'
-  where
-    x' :: Bitvec (n-i) = bvDrop' pri x
diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -4,10 +4,10 @@
 module Language.Hasmtlib.Internal.Parser where
 
 import Prelude hiding (not, (&&), (||), and , or)
-import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
+import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
@@ -16,7 +16,7 @@
 import Data.Coerce
 import Data.Proxy
 import Data.Ratio ((%))
-import Data.ByteString
+import Data.ByteString hiding (filter, foldl)
 import Data.ByteString.Builder
 import Data.Attoparsec.ByteString hiding (Result, skipWhile, takeTill)
 import Data.Attoparsec.ByteString.Char8 hiding (Result)
@@ -91,7 +91,10 @@
   n <- decimal
   _ <- skipSpace >> char ')'
   case someNatVal $ fromInteger n of
-    SomeNat pn -> return $ SomeSMTSort $ SBvSort pn
+    -- SMTLib does not differentiate between signed and unsigned BitVec on the type-level
+    -- We do. So we always just put Unsigned here and in Codec (Expr t)
+    -- if (t ~ BvSort Signed _) we retrieve unsigned solution and flip type-level encoding
+    SomeNat pn -> return $ SomeSMTSort $ SBvSort (Proxy @Unsigned) pn
 {-# INLINEABLE parseSomeBitVecSort #-}
 
 parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
@@ -140,12 +143,13 @@
                       <|> binary "str.prefixof" strPrefixOf <|> binary "str.suffixof" strSuffixOf
                       <|> binary "str.contains" strContains
                       -- TODO: Add compare ops for all (?) bv-sorts
-              SBvSort _ -> unary "bvnot" not
+              SBvSort enc _ -> unary "bvnot" not
                       <|> binary "bvand" (&&)  <|> binary "bvor" (||) <|> binary "bvxor" xor <|> binary "bvnand" BvNand <|> binary "bvnor" BvNor
                       <|> unary  "bvneg" negate
                       <|> binary "bvadd" (+)  <|> binary "bvsub" (-) <|> binary "bvmul" (*)
                       <|> binary "bvudiv" div <|> binary "bvurem" rem
-                      <|> binary "bvshl" BvShL <|> binary "bvlshr" BvLShR
+                      <|> binary "bvshl" BvShL
+                      <|> case bvEncSing' enc of SUnsigned -> binary "bvlshr" BvLShR ; SSigned -> binary "bvashr" BvAShR
               SArraySort _ _ -> ternary "store" ArrStore
                       -- TODO: Add compare ops for all (?) array-sorts
               SStringSort -> binary "str.++" (<>) <|> binary "str.at" strAt <|> ternary "str.substr" StrSubstring
@@ -160,39 +164,39 @@
 
 constant :: forall t. KnownSMTSort t => Parser (HaskellType t)
 constant = case sortSing @t of
-  SIntSort  -> anyValue decimal
-  SRealSort -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational
-  SBoolSort -> parseBool
-  SBvSort p -> anyBitvector p
+  SIntSort       -> anyValue decimal
+  SRealSort      -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational
+  SBoolSort      -> parseBool
+  SBvSort _ p    -> anyBitvector p
   SArraySort k v -> constArray k v
-  SStringSort -> parseSmtString
+  SStringSort    -> parseSmtString
 {-# INLINEABLE constant #-}
 
 constantExpr :: forall t. KnownSMTSort t => Parser (Expr t)
 constantExpr = Constant . wrapValue <$> constant @t
 {-# INLINE constantExpr #-}
 
-anyBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
+anyBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
 anyBitvector p = binBitvector p <|> hexBitvector p <|> literalBitvector p
 {-# INLINE anyBitvector #-}
 
-binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
+binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec enc n)
 binBitvector p = do
   _  <- string "#b" >> skipSpace
   bs <- many $ char '0' <|> char '1'
   let bs' :: [Bit] = fmap (\b -> ite (b == '1') true false) bs
-  case bvFromListN' p bs' of
+  case bitvecFromListN' p bs' of
     Nothing -> fail $ "Expected BitVector of length" <> show (natVal p) <> ", but got a different one"
     Just v  -> return v
 {-# INLINEABLE binBitvector #-}
 
-hexBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
+hexBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
 hexBitvector _ = do
   _ <- string "#x" >> skipSpace
   fromInteger <$> hexadecimal
 {-# INLINE hexBitvector #-}
 
-literalBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
+literalBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
 literalBitvector _ = do
   _ <- char '(' >> skipSpace
   _ <- char '_' >> skipSpace
diff --git a/src/Language/Hasmtlib/Internal/Sharing.hs b/src/Language/Hasmtlib/Internal/Sharing.hs
--- a/src/Language/Hasmtlib/Internal/Sharing.hs
+++ b/src/Language/Hasmtlib/Internal/Sharing.hs
@@ -14,14 +14,13 @@
 import Data.GADT.Compare
 import Data.HashMap.Lazy
 import Data.Default
+import Data.Kind
 import Control.Monad.State
 import Control.Lens
 import System.Mem.StableName
 import System.IO.Unsafe
 import Unsafe.Coerce
 
-import Data.Kind
-
 -- | Mode used for sharing.
 data SharingMode =
     None            -- ^ Common expressions are not shared at all
@@ -60,7 +59,7 @@
         SBoolSort      -> share origExpr expr
         SIntSort       -> share origExpr expr
         SRealSort      -> share origExpr expr
-        SBvSort _      -> share origExpr expr
+        SBvSort _ _    -> share origExpr expr
         SArraySort _ _ -> share origExpr expr
         SStringSort    -> share origExpr expr)
 
diff --git a/src/Language/Hasmtlib/Type/Bitvec.hs b/src/Language/Hasmtlib/Type/Bitvec.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Type/Bitvec.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RoleAnnotations #-}
+
+module Language.Hasmtlib.Type.Bitvec
+( BvEnc(..), SBvEnc(..), KnownBvEnc(..)
+, bvEncSing', bvEncSing''
+, Bitvec(..)
+, asUnsigned, asSigned
+, bitvecConcat, bitvecFromListN, bitvecFromListN'
+)
+where
+
+import Prelude hiding ((&&), (||), not)
+import Language.Hasmtlib.Boolean
+import Language.Hasmtlib.Internal.Render
+import Data.GADT.Compare
+import Data.ByteString.Builder
+import Data.Bit
+import Data.Bits
+import Data.Coerce
+import Data.Finite hiding (shift)
+import Data.Proxy
+import Data.Bifunctor
+import Data.Type.Equality
+import qualified Data.Vector.Unboxed.Sized as V
+import GHC.TypeNats
+
+-- | Type of Bitvector encoding - used as promoted type (data-kind).
+data BvEnc = Unsigned | Signed deriving (Show, Eq, Ord)
+
+-- | Singleton for 'BvEnc'.
+data SBvEnc (enc :: BvEnc) where
+  SUnsigned :: SBvEnc Unsigned
+  SSigned   :: SBvEnc Signed
+
+deriving instance Show (SBvEnc enc)
+deriving instance Eq   (SBvEnc enc)
+deriving instance Ord  (SBvEnc enc)
+
+-- | Compute singleton 'SBvEnc' from it's promoted type 'BvEnc'.
+class KnownBvEnc (enc :: BvEnc) where bvEncSing :: SBvEnc enc
+instance KnownBvEnc Unsigned    where bvEncSing = SUnsigned
+instance KnownBvEnc Signed      where bvEncSing = SSigned
+
+-- | Wrapper for 'bvEncSing' which takes a 'Proxy'.
+bvEncSing' :: forall enc prxy. KnownBvEnc enc => prxy enc -> SBvEnc enc
+bvEncSing' _ = bvEncSing @enc
+
+-- | Wrapper for 'bvEncSing' which takes a 'Proxy' and some ballast.
+--   This is helpful for singing on values of type 'Bitvec' where the ballst is a 'Nat'.
+bvEncSing'' :: forall enc a prxy. KnownBvEnc enc => prxy enc a -> SBvEnc enc
+bvEncSing'' _ = bvEncSing @enc
+
+instance GEq SBvEnc where
+  geq SUnsigned SUnsigned = Just Refl
+  geq SSigned SSigned = Just Refl
+  geq _ _ = Nothing
+
+instance GCompare SBvEnc where
+  gcompare SUnsigned SUnsigned = GEQ
+  gcompare SUnsigned _  = GLT
+  gcompare _ SUnsigned  = GGT
+  gcompare SSigned SSigned = GEQ
+  -- gcompare SSigned _  = GLT
+  -- gcompare _ SSigned  = GGT
+
+-- | Length-indexed bitvector ('V.Vector') carrying a phantom type-level 'BvEnc'.
+--   Most significant bit is first (index 0) for unsigned bitvectors.
+--   Signed bitvectors have their sign bit first (index 0) and their most significant bit second (index 1).
+type role Bitvec phantom phantom
+newtype Bitvec (enc :: BvEnc) (n :: Nat) = Bitvec { unBitvec :: V.Vector n Bit }
+  deriving newtype (Eq, Ord, Boolean)
+
+-- | Convert 'Bitvec' with any encoding 'BvEnc' to 'Unsigned'.
+asUnsigned :: forall enc n. Bitvec enc n -> Bitvec Unsigned n
+asUnsigned = coerce . coerce @(Bitvec enc n) @(V.Vector n Bit)
+
+-- | Convert 'Bitvec' with any encoding 'BvEnc' to 'Signed'.
+asSigned :: forall enc n. Bitvec enc n -> Bitvec Signed n
+asSigned = coerce . coerce @(Bitvec enc n) @(V.Vector n Bit)
+
+instance Show (Bitvec enc n) where
+  show = V.toList . V.map (\b -> if coerce b then '1' else '0') . coerce @_ @(V.Vector n Bit)
+  {-# INLINEABLE show #-}
+
+instance Render (Bitvec enc n) where
+  render = stringUtf8 . show
+  {-# INLINE render #-}
+
+instance (KnownBvEnc enc, KnownNat n) => Bits (Bitvec enc n) where
+  (.&.) = (&&)
+  (.|.) = (||)
+  xor = Language.Hasmtlib.Boolean.xor
+  complement = not
+  shift bv i  = coerce $ shift (coerce @_ @(V.Vector n Bit) bv) (negate i)
+  rotate bv i = coerce $ rotate (coerce @_ @(V.Vector n Bit) bv) (negate i)
+  bitSize _ = fromIntegral $ natVal (Proxy @n)
+  bitSizeMaybe _ = Just $ fromIntegral $ natVal (Proxy @n)
+  isSigned _ = case bvEncSing @enc of
+    SUnsigned -> False
+    SSigned -> True
+  testBit bv = testBit (V.reverse (coerce @_ @(V.Vector n Bit) bv))
+  bit (toInteger -> i) = coerce $ V.reverse $ V.replicate @n (Bit False) V.// [(finite i, Bit True)]
+  popCount = coerce . popCount . coerce @_ @(V.Vector n Bit)
+
+instance (KnownBvEnc enc, KnownNat n) => Num (Bitvec enc n) where
+   fromInteger x = coerce . V.reverse $ V.generate @n (coerce . testBit x . fromInteger . getFinite)
+   negate        = case bvEncSing @enc of
+    SUnsigned -> id
+    SSigned -> (+1) . not
+   abs x         = if signum x < 0 then negate x else x
+   signum x      = case bvEncSing @enc of
+    SUnsigned -> 0
+    SSigned -> if testBit x 0 then -1 else 1
+   x + y = fromInteger $ toInteger x + toInteger y
+   x - y = fromInteger $ toInteger x - toInteger y
+   x * y = fromInteger $ toInteger x * toInteger y
+
+instance (KnownBvEnc enc, KnownNat n) => Bounded (Bitvec enc n) where
+  minBound = case bvEncSing @enc of
+    SUnsigned -> coerce $ V.replicate @n false
+    SSigned -> coerce $ setBit (V.replicate @n false) 0
+  maxBound = case bvEncSing @enc of
+    SUnsigned -> coerce $ V.replicate @n true
+    SSigned -> coerce $ clearBit (V.replicate @n true) 0
+
+instance (KnownBvEnc enc, KnownNat n) => Enum (Bitvec enc n) where
+  toEnum     = fromInteger . toInteger
+  fromEnum x = case bvEncSing @enc of
+    SUnsigned -> V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse $ coerce @_ @(V.Vector n Bit) x
+    SSigned -> if testBit x 0
+          then negate . (+1) . V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse $ coerce @_ @(V.Vector n Bit) $ not x
+          else V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse $ coerce @_ @(V.Vector n Bit) x
+
+instance (KnownBvEnc enc, KnownNat n) => Real (Bitvec enc n) where
+  toRational = toRational . fromEnum
+
+instance (KnownBvEnc enc, KnownNat n) => Integral (Bitvec enc n) where
+  toInteger = fromIntegral . fromEnum
+  quotRem x y = bimap fromInteger fromInteger $ quotRem (toInteger x) (toInteger y)
+
+bitvecConcat :: Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)
+bitvecConcat (coerce -> x) (coerce -> y) = coerce $ x V.++ y
+
+bitvecFromListN :: forall n enc. KnownNat n => [Bit] -> Maybe (Bitvec enc n)
+bitvecFromListN = coerce . V.fromListN @n
+
+bitvecFromListN' :: KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec enc n)
+bitvecFromListN' _ = bitvecFromListN
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -13,7 +13,7 @@
   , equal, distinct
   , for_all, exists
   , select, store
-  , bvShL, bvLShR, bvConcat
+  , bvShL, bvLShR, bvAShR, bvConcat
   , toRealSort, toIntSort, isIntSort
   , strLength, strAt, strSubstring, strPrefixOf, strSuffixOf, strContains, strIndexOf, strReplace, strReplaceAll
   )
@@ -22,6 +22,7 @@
 import Prelude hiding (not, and, or, any, all, (&&), (||))
 import Language.Hasmtlib.Internal.Uniplate1
 import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Type.Bitvec (BvEnc(..), KnownBvEnc(..), SBvEnc(..), bvEncSing')
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Value
@@ -71,6 +72,7 @@
   Mul       :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
   Abs       :: Num (HaskellType t) => Expr t -> Expr t
   Mod       :: Integral (HaskellType t) => Expr t -> Expr t  -> Expr t
+  Rem       :: Integral (HaskellType t) => Expr t -> Expr t  -> Expr t
   IDiv      :: Integral (HaskellType t) => Expr t -> Expr t  -> Expr t
   Div       :: Expr RealSort -> Expr RealSort -> Expr RealSort
   LTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
@@ -97,19 +99,18 @@
   ToInt     :: Expr RealSort -> Expr IntSort
   IsInt     :: Expr RealSort -> Expr BoolSort
   Ite       :: Expr BoolSort -> Expr t -> Expr t -> Expr t
-  BvNand    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvNor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvShL     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvLShR    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvConcat  :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
-  BvRotL    :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)
-  BvRotR    :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)
+  BvNand    :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
+  BvNor     :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
+  BvShL     :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
+  BvLShR    :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n)
+  BvAShR    :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)
+  BvConcat  :: (KnownBvEnc enc , KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
+  BvRotL    :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)
+  BvRotR    :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)
   ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v
   ArrStore  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
   StrConcat     :: Expr StringSort -> Expr StringSort -> Expr StringSort
   StrLength     :: Expr StringSort -> Expr IntSort
-  StrLT         :: Expr StringSort -> Expr StringSort -> Expr BoolSort
-  StrLTHE       :: Expr StringSort -> Expr StringSort -> Expr BoolSort
   StrAt         :: Expr StringSort -> Expr IntSort -> Expr StringSort
   StrSubstring  :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
   StrPrefixOf   :: Expr StringSort -> Expr StringSort -> Expr BoolSort
@@ -118,14 +119,13 @@
   StrIndexOf    :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
   StrReplace    :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
   StrReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
-
   -- | Just v if quantified var has been created already, Nothing otherwise
   ForAll    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
   -- | Just v if quantified var has been created already, Nothing otherwise
   Exists    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
 
-  -- | Indicates whether an expression is a leaf.
-  --   All non-recursive contructors form leafs.
+-- | Indicates whether an expression is a leaf.
+--   All non-recursive contructors form leafs.
 isLeaf :: Expr t -> Bool
 isLeaf (Var _) = True
 isLeaf (Constant _) = True
@@ -310,27 +310,7 @@
 max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
 max' x y = ite (y <=? x) x y
 
-instance Orderable (Expr IntSort) where
-  (<?)     = LTH
-  {-# INLINE (<?) #-}
-  (<=?)    = LTHE
-  {-# INLINE (<=?) #-}
-  (>=?)    = GTHE
-  {-# INLINE (>=?) #-}
-  (>?)     = GTH
-  {-# INLINE (>?) #-}
-
-instance Orderable (Expr RealSort) where
-  (<?)     = LTH
-  {-# INLINE (<?) #-}
-  (<=?)    = LTHE
-  {-# INLINE (<=?) #-}
-  (>=?)    = GTHE
-  {-# INLINE (>=?) #-}
-  (>?)     = GTH
-  {-# INLINE (>?) #-}
-
-instance KnownNat n => Orderable (Expr (BvSort n)) where
+instance (KnownSMTSort t, Ord (HaskellType t)) => Orderable (Expr t) where
   (<?)     = LTH
   {-# INLINE (<?) #-}
   (<=?)    = LTHE
@@ -340,13 +320,6 @@
   (>?)     = GTH
   {-# INLINE (>?) #-}
 
--- | Lexicographic ordering for '(<?)' and reflexive closure of lexicographic ordering for '(<=?)'
-instance Orderable (Expr StringSort) where
-  (<?)     = StrLT
-  {-# INLINE (<?) #-}
-  (<=?)    = StrLTHE
-  {-# INLINE (<=?) #-}
-
 class GEquatable f => GOrderable f where
   (<?#)  :: f a -> f a -> Expr BoolSort
   (<=?#) :: f a -> f a -> Expr BoolSort
@@ -504,18 +477,23 @@
 store = ArrStore
 {-# INLINE store #-}
 
--- | Bitvector shift left
-bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+-- | Logically shift left the first expression by the second expression.
+bvShL    :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
 bvShL    = BvShL
 {-# INLINE bvShL #-}
 
--- | Bitvector logical shift right
-bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+-- | Logically shift right the first expression by the second expression.
+bvLShR   :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n)
 bvLShR   = BvLShR
 {-# INLINE bvLShR #-}
 
--- | Concat two bitvectors
-bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
+-- | Arithmetically shift right the first expression by the second expression.
+bvAShR   :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)
+bvAShR   = BvAShR
+{-# INLINE bvAShR #-}
+
+-- | Concats two bitvectors.
+bvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
 bvConcat = BvConcat
 {-# INLINE bvConcat #-}
 
@@ -596,92 +574,50 @@
 strReplaceAll = StrReplaceAll
 {-# INLINE strReplaceAll #-}
 
-instance Num (Expr IntSort) where
-   fromInteger = Constant . IntValue
-   {-# INLINE fromInteger #-}
-   (Constant (IntValue 0)) + y = y
-   x + (Constant (IntValue 0)) = x
-   (Constant (IntValue x)) + (Constant (IntValue y)) = Constant (IntValue (x + y))
-   x + y = Plus x y
-   {-# INLINE (+) #-}
-   x - (Constant (IntValue 0)) = x
-   (Constant (IntValue x)) - (Constant (IntValue y)) = Constant (IntValue (x - y))
-   x - y = Minus x y
-   {-# INLINE (-) #-}
-   (Constant (IntValue 0)) * _ = 0
-   _ * (Constant (IntValue 0)) = 0
-   (Constant (IntValue 1)) * y = y
-   x * (Constant (IntValue 1)) = x
-   (Constant (IntValue x)) * (Constant (IntValue y)) = Constant (IntValue (x * y))
-   x * y = Mul x y
-   {-# INLINE (*) #-}
-   negate      = Neg
-   {-# INLINE negate #-}
-   abs         = Abs
-   {-# INLINE abs #-}
-   signum x    = ite (x === 0) 0 $ ite (x <? 0) (-1) 1
-   {-# INLINE signum #-}
-
-instance Num (Expr RealSort) where
-   fromInteger = Constant . RealValue . fromIntegral
+instance (KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Num (Expr t) where
+   fromInteger = Constant . wrapValue . fromInteger
    {-# INLINE fromInteger #-}
-   (Constant (RealValue 0)) + y = y
-   x + (Constant (RealValue 0)) = x
-   (Constant (RealValue x)) + (Constant (RealValue y)) = Constant (RealValue (x + y))
+   (Constant 0) + y = y
+   x + (Constant 0) = x
+   (Constant x) + (Constant y) = Constant (x + y)
    x + y = Plus x y
    {-# INLINE (+) #-}
-   x - (Constant (RealValue 0)) = x
-   (Constant (RealValue x)) - (Constant (RealValue y)) = Constant (RealValue (x - y))
+   x - (Constant 0) = x
+   (Constant x) - (Constant y) = Constant (x - y)
+   (Constant 0) - x = negate x
    x - y = Minus x y
    {-# INLINE (-) #-}
-   (Constant (RealValue 0)) * _ = 0
-   _ * (Constant (RealValue 0)) = 0
-   (Constant (RealValue 1)) * y = y
-   x * (Constant (RealValue 1)) = x
-   (Constant (RealValue x)) * (Constant (RealValue y)) = Constant (RealValue (x * y))
+   (Constant 0) * _ = 0
+   _ * (Constant 0) = 0
+   (Constant 1) * y = y
+   x * (Constant 1) = x
+   (Constant (-1)) * x = negate x
+   x * (Constant (-1)) = negate x
+   (Constant x) * (Constant y) = Constant (x * y)
    x * y = Mul x y
    {-# INLINE (*) #-}
-   negate      = Neg
+   negate (Constant x) = Constant $ negate x
+   negate (Neg x)      = x
+   negate x            = Neg x
    {-# INLINE negate #-}
-   abs         = Abs
-   {-# INLINE abs #-}
-   signum x    = ite (x === 0) 0 $ ite (x <? 0) (-1) 1
-   {-# INLINE signum #-}
-
-instance KnownNat n => Num (Expr (BvSort n)) where
-   fromInteger = Constant . BvValue . fromInteger
-   {-# INLINE fromInteger #-}
-   (Constant (BvValue 0)) + y = y
-   x + (Constant (BvValue 0)) = x
-   (Constant (BvValue x)) + (Constant (BvValue y)) = Constant (BvValue (x + y))
-   x + y = Plus x y
-   {-# INLINE (+) #-}
-   x - (Constant (BvValue 0)) = x
-   (Constant (BvValue x)) - (Constant (BvValue y)) = Constant (BvValue (x - y))
-   x - y = Minus x y
-   {-# INLINE (-) #-}
-   (Constant (BvValue 0)) * _ = 0
-   _ * (Constant (BvValue 0)) = 0
-   (Constant (BvValue 1)) * y = y
-   x * (Constant (BvValue 1)) = x
-   (Constant (BvValue x)) * (Constant (BvValue y)) = Constant (BvValue (x * y))
-   x * y = Mul x y
-   {-# INLINE (*) #-}
-   abs         = id
+   abs (Constant x) = Constant $ abs x
+   abs x            = Abs x
    {-# INLINE abs #-}
-   signum _    = 0
+   signum (Constant x) = Constant $ signum x
+   signum x            = ite (x === 0) 0 $ ite (x <? 0) (-1) 1
    {-# INLINE signum #-}
 
 instance Fractional (Expr RealSort) where
   fromRational = Constant . RealValue . fromRational
   {-# INLINE fromRational #-}
-  x / (Constant (RealValue 1)) = x
-  (Constant (RealValue 0)) / _ = 0
-  (Constant (RealValue x)) / (Constant (RealValue y)) = Constant (RealValue (x / y))
+  x / (Constant  1) = x
+  (Constant 0) / _ = 0
+  (Constant x) / (Constant y) = Constant (x / y)
   x / y          = Div x y
   {-# INLINE (/) #-}
 
--- | Not in the SMTLib2.6-standard. Solvers like CVC5 and MathSAT support it though.
+-- | Not part of the SMTLib standard Version 2.6.
+--   Some solvers support it. At least valid for CVC5 and MathSAT.
 instance Floating (Expr RealSort) where
     pi    = Pi
     {-# INLINE pi #-}
@@ -709,106 +645,61 @@
     acosh = error "SMT-Solvers currently do not support acosh"
     atanh = error "SMT-Solvers currently do not support atanh"
 
--- | This instance is __partial__ for 'toRational', it's only intended for use with constants ('Constant').
-instance Real (Expr IntSort) where
-  toRational (Constant (IntValue x)) = fromIntegral x
-  toRational x = error $ "Real#toRational[Expr IntSort] only supported for constants. But given: " <> show x
-  {-# INLINE toRational #-}
-
--- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant').
-instance Enum (Expr IntSort) where
-  fromEnum (Constant (IntValue x)) = fromIntegral x
-  fromEnum x = error $ "Enum#fromEnum[Expr IntSort] only supported for constants. But given: " <> show x
-  {-# INLINE fromEnum #-}
-  toEnum = fromInteger . fromIntegral
-  {-# INLINE toEnum #-}
-
--- | This instance is __partial__ for 'toInteger', it's only intended for use with constants ('Constant').
-instance Integral (Expr IntSort) where
-  quot = IDiv
-  {-# INLINE quot #-}
-  rem  = Mod
-  {-# INLINE rem #-}
-  div  = IDiv
-  {-# INLINE div #-}
-  mod  = Mod
-  {-# INLINE mod #-}
-  quotRem x y = (quot x y, rem x y)
-  {-# INLINE quotRem #-}
-  divMod x y  = (div x y, mod x y)
-  {-# INLINE divMod #-}
-  toInteger (Constant (IntValue x)) = x
-  toInteger x = error $ "Integer#toInteger[Expr IntSort] only supported for constants. But given: " <> show x
-  {-# INLINE toInteger #-}
-
--- | This instance is __partial__ for 'toRational', it's only intended for use with constants ('Constant').
-instance Real (Expr RealSort) where
-  toRational (Constant (RealValue x)) = toRational x
-  toRational x = error $ "Real#toRational[Expr RealSort] only supported for constants. But given: " <> show x
-  {-# INLINE toRational #-}
-
--- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant').
-instance Enum (Expr RealSort) where
-  fromEnum (Constant (RealValue x)) = fromEnum x
-  fromEnum x = error $ "Enum#fromEnum[Expr RealSort] only supported for constants. But given: " <> show x
-  {-# INLINE fromEnum #-}
-  toEnum = fromInteger . fromIntegral
-  {-# INLINE toEnum #-}
-
--- | This instance is __partial__ for 'toRational', it's only intended for use with constants ('Constant').
-instance KnownNat n => Real (Expr (BvSort n)) where
-  toRational (Constant (BvValue x)) = fromIntegral x
-  toRational x = error $ "Real#toRational[Expr BvSort] only supported for constants. But given: " <> show x
+-- | This instance is __partial__ for 'toRational', this method is only intended for use with constants.
+instance (KnownSMTSort t, Real (HaskellType t)) => Real (Expr t) where
+  toRational (Constant x) = toRational $ unwrapValue x
+  toRational x = error $ "Real#toRational[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x
   {-# INLINE toRational #-}
 
--- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant').
-instance KnownNat n => Enum (Expr (BvSort n)) where
-  fromEnum (Constant (BvValue x)) = fromIntegral x
-  fromEnum x = error $ "Enum#fromEnum[Expr BvSort] only supported for constants. But given: " <> show x
+-- | This instance is __partial__ for 'fromEnum', this method is only intended for use with constants.
+instance (KnownSMTSort t, Enum (HaskellType t)) => Enum (Expr t) where
+  fromEnum (Constant x) = fromEnum $ unwrapValue x
+  fromEnum x = error $ "Enum#fromEnum[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x
   {-# INLINE fromEnum #-}
-  toEnum = fromInteger . fromIntegral
+  toEnum = Constant . wrapValue . toEnum
   {-# INLINE toEnum #-}
 
--- | This instance is __partial__ for 'toInteger', it's only intended for use with constants ('Constant').
-instance KnownNat n => Integral (Expr (BvSort n)) where
-  quot        = IDiv
-  {-# INLINE quot #-}
-  rem         = Mod
-  {-# INLINE rem #-}
-  div         = IDiv
-  {-# INLINE div #-}
-  mod         = Mod
-  {-# INLINE mod #-}
-  quotRem x y = (quot x y, rem x y)
+-- | This instance is __partial__ for 'toInteger', this method is only intended for use with constants.
+instance (KnownSMTSort t, Integral (HaskellType t)) => Integral (Expr t) where
+  quotRem x y = (IDiv x y, Rem x y)
   {-# INLINE quotRem #-}
-  divMod x y  = (div x y, mod x y)
+  divMod x y  = (IDiv x y, Mod x y)
   {-# INLINE divMod #-}
-  toInteger (Constant (BvValue x)) = fromIntegral x
-  toInteger x = error $ "Integer#toInteger[Expr BvSort] only supported for constants. But given: " <> show x
+  toInteger (Constant x) = toInteger $ unwrapValue x
+  toInteger x = error $ "Integer#toInteger[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x
   {-# INLINE toInteger #-}
 
 instance Boolean (Expr BoolSort) where
   bool = Constant . BoolValue
   {-# INLINE bool #-}
-  (&&) = And
+  (Constant (BoolValue x)) && y = if x then y else false
+  x && (Constant (BoolValue y)) = if y then x else false
+  x && y = And x y
   {-# INLINE (&&) #-}
-  (||) = Or
+  (Constant (BoolValue x)) || y = if x then true else y
+  x || (Constant (BoolValue y)) = if y then true else x
+  x || y = Or x y
   {-# INLINE (||) #-}
-  not  = Not
+  not (Constant x) = Constant $ not x
+  not (Not x) = x
+  not x = Not x
   {-# INLINE not #-}
-  xor  = Xor
+  xor (Constant (BoolValue x)) y  = if x then not y else y
+  xor x (Constant (BoolValue y)) = if y then not x else x
+  xor x y = Xor x y
   {-# INLINE xor #-}
   (<==>) = (===)
   {-# INLINE (<==>) #-}
 
-instance KnownNat n => Boolean (Expr (BvSort n)) where
+instance (KnownBvEnc enc, KnownNat n) => Boolean (Expr (BvSort enc n)) where
   bool = Constant . BvValue . bool
   {-# INLINE bool #-}
   (&&) = And
   {-# INLINE (&&) #-}
   (||) = Or
   {-# INLINE (||) #-}
-  not  = Not
+  not (Not x) = x
+  not x = Not x
   {-# INLINE not #-}
   xor  = Xor
   {-# INLINE xor #-}
@@ -819,7 +710,7 @@
   maxBound = true
   {-# INLINE maxBound #-}
 
-instance KnownNat n => Bounded (Expr (BvSort n)) where
+instance (KnownBvEnc enc, KnownNat n) => Bounded (Expr (BvSort enc n)) where
   minBound = Constant $ BvValue minBound
   {-# INLINE minBound #-}
   maxBound = Constant $ BvValue maxBound
@@ -869,7 +760,7 @@
   {-# INLINE popCount #-}
 
 -- | This instance is __partial__ for 'testBit' and 'popCount', it's only intended for use with constants ('Constant').
-instance KnownNat n => Bits.Bits (Expr (BvSort n)) where
+instance (KnownBvEnc enc, KnownNat n) => Bits.Bits (Expr (BvSort enc n)) where
   (.&.) = And
   {-# INLINE (.&.) #-}
   (.|.) = Or
@@ -889,11 +780,15 @@
   {-# INLINE bitSizeMaybe #-}
   bitSize _ = fromIntegral $ natVal $ Proxy @n
   {-# INLINE bitSize #-}
-  isSigned _ = False
+  isSigned _ = case bvEncSing @enc of
+    SUnsigned -> False
+    SSigned   -> True
   {-# INLINE isSigned #-}
   shiftL b i = BvShL b (fromIntegral i)
   {-# INLINE shiftL #-}
-  shiftR b i = BvLShR b (fromIntegral i)
+  shiftR b i = case bvEncSing @enc of
+    SUnsigned -> BvLShR b (fromIntegral i)
+    SSigned   -> BvAShR b (fromIntegral i)
   {-# INLINE shiftR #-}
   rotateL b i = BvRotL i b
   {-# INLINE rotateL #-}
@@ -940,29 +835,68 @@
 instance KnownSMTSort t => Render (Expr t) where
   render (Var v)      = render v
   render (Constant c) = render c
-
-  render (Plus x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvadd" ; _ -> "+") x y
-  render (Minus x y)  = renderBinary (case sortSing' x of SBvSort _ -> "bvsub" ; _ -> "-") x y
-  render (Neg x)      = renderUnary  (case sortSing' x of SBvSort _ -> "bvneg" ; _ -> "-") x
-  render (Mul x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvmul" ; _ -> "*") x y
+  render (Plus x y)   = renderBinary (case sortSing' x of SBvSort _ _ -> "bvadd" ; _ -> "+") x y
+  render (Minus x y)  = renderBinary (case sortSing' x of SBvSort _ _ -> "bvsub" ; _ -> "-") x y
+  render (Neg x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvneg" ; _ -> "-") x
+  render (Mul x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvmul" ; _ -> "*") x y
   render (Abs x)      = renderUnary  "abs" x
-  render (Mod x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvurem" ; _ -> "mod") x y
-  render (IDiv x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvudiv" ; _ -> "div") x y
+  render (Mod x y)    = renderBinary opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvurem"
+          SSigned -> "bvsmod"
+        _ -> "mod"
+  render (Rem x y)    = renderBinary opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvurem"
+          SSigned -> "bvsrem"
+        _ -> "rem"
+  render (IDiv x y)   = renderBinary opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvudiv"
+          SSigned -> "bvsdiv"
+        _ -> "div"
   render (Div x y)    = renderBinary "/" x y
-
-  render (LTH x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvult" ; _ -> "<") x y
-  render (LTHE x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvule" ; _ -> "<=") x y
+  render (LTH x y)    = renderBinary opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvult"
+          SSigned -> "bvslt"
+        SStringSort -> "str.<"
+        _ -> "<"
+  render (LTHE x y)   = renderBinary opStr x y
+    where
+      opStr = case sortSing' x of
+        SBvSort enc _ -> case bvEncSing' enc of
+          SUnsigned -> "bvule"
+          SSigned -> "bvsle"
+        SStringSort -> "str.<="
+        _ -> "<="
   render (EQU xs)     = renderNary "=" $ V.toList xs
   render (Distinct xs)= renderNary "distinct" $ V.toList xs
-  render (GTHE x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvuge" ; _ -> ">=") x y
-  render (GTH x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvugt" ; _ -> ">") x y
-
-  render (Not x)      = renderUnary  (case sortSing' x of SBvSort _ -> "bvnot" ; _ -> "not") x
-  render (And x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvand" ; _ -> "and") x y
-  render (Or x y)     = renderBinary (case sortSing' x of SBvSort _ -> "bvor" ; _ -> "or") x y
+  render (GTHE x y)   = case sortSing' x of
+    SBvSort enc _ -> case bvEncSing' enc of
+      SUnsigned -> renderBinary "bvuge" x y
+      SSigned   -> renderBinary "bvsge" x y
+    SStringSort -> renderBinary "str.<=" y x
+    _           -> renderBinary ">=" x y
+  render (GTH x y)    = case sortSing' x of
+    SBvSort enc _ -> case bvEncSing' enc of
+      SUnsigned -> renderBinary "bvugt" x y
+      SSigned   -> renderBinary "bvsgt" x y
+    SStringSort -> renderBinary "str.<" y x
+    _           -> renderBinary ">" x y
+  render (Not x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvnot" ; _ -> "not") x
+  render (And x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvand" ; _ -> "and") x y
+  render (Or x y)     = renderBinary (case sortSing' x of SBvSort _ _ -> "bvor" ; _ -> "or") x y
   render (Impl x y)   = renderBinary "=>" x y
-  render (Xor x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvxor" ; _ -> "xor") x y
-
+  render (Xor x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvxor" ; _ -> "xor") x y
   render Pi           = "real.pi"
   render (Sqrt x)     = renderUnary "sqrt" x
   render (Exp x)      = renderUnary "exp" x
@@ -972,28 +906,22 @@
   render (Asin x)     = renderUnary "arcsin" x
   render (Acos x)     = renderUnary "arccos" x
   render (Atan x)     = renderUnary "arctan" x
-
   render (ToReal x)   = renderUnary "to_real" x
   render (ToInt x)    = renderUnary "to_int" x
   render (IsInt x)    = renderUnary "is_int" x
-
   render (Ite p t f)  = renderTernary "ite" p t f
-
   render (BvNand x y)       = renderBinary "bvnand" (render x) (render y)
   render (BvNor x y)        = renderBinary "bvnor"  (render x) (render y)
   render (BvShL x y)        = renderBinary "bvshl"  (render x) (render y)
   render (BvLShR x y)       = renderBinary "bvlshr" (render x) (render y)
+  render (BvAShR x y)       = renderBinary "bvashr" (render x) (render y)
   render (BvConcat x y)     = renderBinary "concat" (render x) (render y)
   render (BvRotL i x)       = renderUnary (renderBinary "_" ("rotate_left"  :: Builder) (render $ toInteger i)) (render x)
   render (BvRotR i x)       = renderUnary (renderBinary "_" ("rotate_right" :: Builder) (render $ toInteger i)) (render x)
-
   render (ArrSelect a i)    = renderBinary  "select" (render a) (render i)
   render (ArrStore a i v)   = renderTernary "store"  (render a) (render i) (render v)
-
   render (StrConcat x y)        = renderBinary "str.++"  (render x) (render y)
   render (StrLength x)          = renderUnary  "str.len" (render x)
-  render (StrLT x y)            = renderBinary "str.<"   (render x) (render y)
-  render (StrLTHE x y)          = renderBinary "str.<="  (render x) (render y)
   render (StrAt x i)            = renderBinary "str.at"  (render x) (render i)
   render (StrSubstring x i j)   = renderTernary "str.substr"  (render x) (render i) (render j)
   render (StrPrefixOf x y)      = renderBinary "str.prefixof" (render x) (render y)
@@ -1002,7 +930,6 @@
   render (StrIndexOf x y i)     = renderTernary "str.indexof"     (render x) (render y) (render i)
   render (StrReplace x y y')    = renderTernary "str.replace"     (render x) (render y) (render y')
   render (StrReplaceAll x y y') = renderTernary "str.replace_all" (render x) (render y) (render y')
-
   render (ForAll mQvar f) = renderQuantifier "forall" mQvar f
   render (Exists mQvar f) = renderQuantifier "exists" mQvar f
 
@@ -1072,6 +999,7 @@
   uniplate1 f (Mul x y)               = Mul <$> f x <*> f y
   uniplate1 f (Abs x)                 = Abs <$> f x
   uniplate1 f (Mod x y)               = Mod <$> f x <*> f y
+  uniplate1 f (Rem x y)               = Rem <$> f x <*> f y
   uniplate1 f (IDiv x y)              = IDiv <$> f x <*> f y
   uniplate1 f (Div x y)               = Div <$> f x <*> f y
   uniplate1 f (LTH x y)               = LTH <$> f x <*> f y
@@ -1102,6 +1030,7 @@
   uniplate1 f (BvNor x y)             = BvNor <$> f x <*> f y
   uniplate1 f (BvShL x y)             = BvShL <$> f x <*> f y
   uniplate1 f (BvLShR x y)            = BvLShR <$> f x <*> f y
+  uniplate1 f (BvAShR x y)            = BvAShR <$> f x <*> f y
   uniplate1 f (BvConcat x y)          = BvConcat <$> f x <*> f y
   uniplate1 f (BvRotL i x)            = BvRotL i <$> f x
   uniplate1 f (BvRotR i x)            = BvRotR i <$> f x
@@ -1109,8 +1038,6 @@
   uniplate1 f (ArrStore i x arr)      = ArrStore i <$> f x <*> f arr
   uniplate1 f (StrConcat x y)         = StrConcat <$> f x <*> f y
   uniplate1 f (StrLength x)           = StrLength <$> f x
-  uniplate1 f (StrLT x y)             = StrLT <$> f x <*> f y
-  uniplate1 f (StrLTHE x y)           = StrLTHE <$> f x <*> f y
   uniplate1 f (StrAt x i)             = StrAt <$> f x <*> f i
   uniplate1 f (StrSubstring x i j)    = StrSubstring <$> f x <*> f i <*> f j
   uniplate1 f (StrPrefixOf x y)       = StrPrefixOf <$> f x <*> f y
@@ -1140,6 +1067,7 @@
           Mul x y              -> Mul  <$> tryPlate f' x <*> tryPlate f' y
           Abs x                -> Abs  <$> tryPlate f' x
           Mod x y              -> Mod  <$> tryPlate f' x <*> tryPlate f' y
+          Rem x y              -> Mod  <$> tryPlate f' x <*> tryPlate f' y
           IDiv x y             -> IDiv <$> tryPlate f' x <*> tryPlate f' y
           Div x y              -> Div  <$> tryPlate f' x <*> tryPlate f' y
           LTH x y              -> LTH  <$> tryPlate f' x <*> tryPlate f' y
@@ -1170,6 +1098,7 @@
           BvNor x y            -> BvNor  <$> tryPlate f' x <*> tryPlate f' y
           BvShL x y            -> BvShL  <$> tryPlate f' x <*> tryPlate f' y
           BvLShR x y           -> BvLShR <$> tryPlate f' x <*> tryPlate f' y
+          BvAShR x y           -> BvAShR <$> tryPlate f' x <*> tryPlate f' y
           BvConcat x y         -> BvConcat <$> tryPlate f' x <*> tryPlate f' y
           BvRotL i x           -> BvRotL i <$> tryPlate f' x
           BvRotR i x           -> BvRotR i <$> tryPlate f' x
@@ -1177,8 +1106,6 @@
           ArrStore i x arr     -> ArrStore i    <$> tryPlate f' x <*> tryPlate f' arr
           StrConcat x y        -> StrConcat     <$> tryPlate f' x <*> tryPlate f' y
           StrLength x          -> StrLength     <$> tryPlate f' x
-          StrLT x y            -> StrLT         <$> tryPlate f' x <*> tryPlate f' y
-          StrLTHE x y          -> StrLTHE       <$> tryPlate f' x <*> tryPlate f' y
           StrAt x i            -> StrAt         <$> tryPlate f' x <*> tryPlate f' i
           StrSubstring x i j   -> StrSubstring  <$> tryPlate f' x <*> tryPlate f' i <*> tryPlate f' j
           StrPrefixOf x y      -> StrPrefixOf   <$> tryPlate f' x <*> tryPlate f' y
@@ -1202,6 +1129,7 @@
     Mul e1 e2            -> grnf e1 `seq` grnf e2
     Abs e                -> grnf e
     Mod e1 e2            -> grnf e1 `seq` grnf e2
+    Rem e1 e2            -> grnf e1 `seq` grnf e2
     IDiv e1 e2           -> grnf e1 `seq` grnf e2
     Div e1 e2            -> grnf e1 `seq` grnf e2
     LTH e1 e2            -> grnf e1 `seq` grnf e2
@@ -1232,6 +1160,7 @@
     BvNor e1 e2          -> grnf e1 `seq` grnf e2
     BvShL e1 e2          -> grnf e1 `seq` grnf e2
     BvLShR e1 e2         -> grnf e1 `seq` grnf e2
+    BvAShR e1 e2         -> grnf e1 `seq` grnf e2
     BvConcat e1 e2       -> grnf e1 `seq` grnf e2
     BvRotL _ e           -> grnf e
     BvRotR _ e           -> grnf e
@@ -1239,8 +1168,6 @@
     ArrStore e1 e2 e3    -> grnf e1 `seq` grnf e2 `seq` grnf e3
     StrConcat e1 e2      -> grnf e1 `seq` grnf e2
     StrLength e          -> grnf e
-    StrLT e1 e2          -> grnf e1 `seq` grnf e2
-    StrLTHE e1 e2        -> grnf e1 `seq` grnf e2
     StrAt e1 e2          -> grnf e1 `seq` grnf e2
     StrSubstring e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3
     StrPrefixOf e1 e2    -> grnf e1 `seq` grnf e2
@@ -1300,6 +1227,9 @@
   gcompare (Mod x y) (Mod x' y') = gcomparing [(x,x'), (y,y')]
   gcompare (Mod _ _) _ = GLT
   gcompare _ (Mod _ _) = GGT
+  gcompare (Rem x y) (Rem x' y') = gcomparing [(x,x'), (y,y')]
+  gcompare (Rem _ _) _ = GLT
+  gcompare _ (Rem _ _) = GGT
   gcompare (IDiv x y) (IDiv x' y') = gcomparing [(x,x'), (y,y')]
   gcompare (IDiv _ _) _ = GLT
   gcompare _ (IDiv _ _) = GGT
@@ -1426,6 +1356,9 @@
   gcompare (BvLShR x y)            (BvLShR x' y')          = gcomparing [(x,x'), (y,y')]
   gcompare (BvLShR _ _) _ = GLT
   gcompare _ (BvLShR _ _) = GGT
+  gcompare (BvAShR x y)            (BvAShR x' y')          = gcomparing [(x,x'), (y,y')]
+  gcompare (BvAShR _ _) _ = GLT
+  gcompare _ (BvAShR _ _) = GGT
   gcompare (BvConcat x y)          (BvConcat x' y')        = case gcompare (sortSing' x) (sortSing' x') of
     GLT -> GLT
     GEQ -> case gcompare x x' of
@@ -1483,18 +1416,6 @@
     GGT -> GGT
   gcompare (StrLength _) _ = GLT
   gcompare _ (StrLength _) = GGT
-  gcompare (StrLT x y)             (StrLT x' y')           = case gcomparing [(x,x'), (y,y')] of
-    GLT -> GLT
-    GEQ -> GEQ
-    GGT -> GGT
-  gcompare (StrLT _ _) _ = GLT
-  gcompare _ (StrLT _ _) = GGT
-  gcompare (StrLTHE x y)           (StrLTHE x' y')         = case gcomparing [(x,x'), (y,y')] of
-    GLT -> GLT
-    GEQ -> GEQ
-    GGT -> GGT
-  gcompare (StrLTHE _ _) _ = GLT
-  gcompare _ (StrLTHE _ _) = GGT
   gcompare (StrAt x i)             (StrAt x' i')           = case gcompare x x' of
     GLT -> GLT
     GEQ -> case gcompare i i' of
diff --git a/src/Language/Hasmtlib/Type/SMTSort.hs b/src/Language/Hasmtlib/Type/SMTSort.hs
--- a/src/Language/Hasmtlib/Type/SMTSort.hs
+++ b/src/Language/Hasmtlib/Type/SMTSort.hs
@@ -5,7 +5,7 @@
 module Language.Hasmtlib.Type.SMTSort where
 
 import Language.Hasmtlib.Internal.Constraint
-import Language.Hasmtlib.Internal.Bitvec
+import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.ArrayMap
 import Data.GADT.Compare
@@ -21,7 +21,7 @@
     BoolSort                      -- ^ Sort of Bool
   | IntSort                       -- ^ Sort of Int
   | RealSort                      -- ^ Sort of Real
-  | BvSort Nat                    -- ^ Sort of BitVec with length n
+  | BvSort BvEnc Nat              -- ^ Sort of BitVec with type of encoding enc and length n
   | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v
   | StringSort                    -- ^ Sort of String
 
@@ -30,7 +30,7 @@
   HaskellType IntSort         = Integer
   HaskellType RealSort        = Double
   HaskellType BoolSort        = Bool
-  HaskellType (BvSort n)      = Bitvec n
+  HaskellType (BvSort enc n)  = Bitvec enc n
   HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)
   HaskellType StringSort      = Text.Text
 
@@ -39,7 +39,7 @@
   SIntSort    :: SSMTSort IntSort
   SRealSort   :: SSMTSort RealSort
   SBoolSort   :: SSMTSort BoolSort
-  SBvSort     :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
+  SBvSort     :: (KnownBvEnc enc, KnownNat n) => Proxy enc -> Proxy n -> SSMTSort (BvSort enc n)
   SArraySort  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
   SStringSort :: SSMTSort StringSort
 
@@ -51,9 +51,11 @@
   geq SIntSort SIntSort       = Just Refl
   geq SRealSort SRealSort     = Just Refl
   geq SBoolSort SBoolSort     = Just Refl
-  geq (SBvSort n) (SBvSort m) = case sameNat n m of
+  geq (SBvSort enc n) (SBvSort emc m) = case sameNat n m of
     Nothing   -> Nothing
-    Just Refl -> Just Refl
+    Just Refl -> case geq (bvEncSing' enc) (bvEncSing' emc) of
+      Nothing -> Nothing
+      Just Refl -> Just Refl
   geq (SArraySort k v) (SArraySort k' v') = case geq (sortSing' k) (sortSing' k') of
     Nothing   -> Nothing
     Just Refl -> case geq (sortSing' v) (sortSing' v') of
@@ -66,9 +68,12 @@
   gcompare SBoolSort SBoolSort     = GEQ
   gcompare SIntSort SIntSort       = GEQ
   gcompare SRealSort SRealSort     = GEQ
-  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of
+  gcompare (SBvSort enc n) (SBvSort emc m) = case cmpNat n m of
     LTI -> GLT
-    EQI -> GEQ
+    EQI -> case gcompare (bvEncSing' enc) (bvEncSing' emc) of
+      GLT -> GLT
+      GEQ -> GEQ
+      GGT -> GGT
     GTI -> GGT
   gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of
     GLT -> GLT
@@ -94,12 +99,12 @@
 instance KnownSMTSort IntSort                  where sortSing = SIntSort
 instance KnownSMTSort RealSort                 where sortSing = SRealSort
 instance KnownSMTSort BoolSort                 where sortSing = SBoolSort
-instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)
+instance (KnownBvEnc enc, KnownNat n) => KnownSMTSort (BvSort enc n) where sortSing = SBvSort (Proxy @enc) (Proxy @n)
 instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => KnownSMTSort (ArraySort k v) where
    sortSing = SArraySort (Proxy @k) (Proxy @v)
 instance KnownSMTSort StringSort                 where sortSing = SStringSort
 
--- | Wrapper for 'sortSing' which takes a 'Proxy'
+-- | Wrapper for 'sortSing' which takes a 'Proxy'.
 sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
 sortSing' _ = sortSing @t
 
@@ -116,7 +121,7 @@
   render SBoolSort   = "Bool"
   render SIntSort    = "Int"
   render SRealSort   = "Real"
-  render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
+  render (SBvSort _ p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
   render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)
   render SStringSort   = "String"
   {-# INLINEABLE render #-}
diff --git a/src/Language/Hasmtlib/Type/Value.hs b/src/Language/Hasmtlib/Type/Value.hs
--- a/src/Language/Hasmtlib/Type/Value.hs
+++ b/src/Language/Hasmtlib/Type/Value.hs
@@ -6,7 +6,10 @@
 )
 where
 
+import Prelude hiding (not, (&&), (||))
 import Language.Hasmtlib.Type.SMTSort
+import Language.Hasmtlib.Type.Bitvec
+import Language.Hasmtlib.Boolean
 import Data.GADT.Compare
 import Data.Proxy
 import Control.Lens
@@ -18,7 +21,7 @@
   IntValue    :: HaskellType IntSort    -> Value IntSort
   RealValue   :: HaskellType RealSort   -> Value RealSort
   BoolValue   :: HaskellType BoolSort   -> Value BoolSort
-  BvValue     :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort n)
+  BvValue     :: (KnownBvEnc enc, KnownNat n) => HaskellType (BvSort enc n) -> Value (BvSort enc n)
   ArrayValue  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
   StringValue :: HaskellType StringSort -> Value StringSort
 
@@ -30,7 +33,9 @@
   geq (IntValue x) (IntValue y)     = if x == y then Just Refl else Nothing
   geq (RealValue x) (RealValue y)   = if x == y then Just Refl else Nothing
   geq (BvValue x) (BvValue y)       = case cmpNat x y of
-    EQI -> if x == y then Just Refl else Nothing
+    EQI -> case geq (bvEncSing'' x) (bvEncSing'' y) of
+      Nothing -> Nothing
+      Just Refl -> if x == y then Just Refl else Nothing
     _   -> Nothing
   geq ax@(ArrayValue x) ay@(ArrayValue y) = case geq (sortSing' ax) (sortSing' ay) of
     Nothing -> Nothing
@@ -50,7 +55,10 @@
   gcompare (RealValue x) (RealValue x')     = liftOrdering $ compare x x'
   gcompare (BvValue x) (BvValue x')         = case cmpNat x x' of
     LTI -> GLT
-    EQI -> liftOrdering $ compare x x'
+    EQI -> case gcompare (bvEncSing'' x) (bvEncSing'' x') of
+      GLT -> GLT
+      GEQ -> liftOrdering $ compare x x'
+      GGT -> GGT
     GTI -> GGT
   gcompare (ArrayValue x) (ArrayValue x')   = case gcompare (sortSing' (pk x)) (sortSing' (pk x')) of
     GLT -> GLT
@@ -78,6 +86,40 @@
   -- gcompare (StringValue _) _                = GLT
   -- gcompare _ (StringValue _)                = GGT
 
+instance (KnownSMTSort t, Num (HaskellType t)) => Num (Value t) where
+  fromInteger = wrapValue . fromInteger
+  {-# INLINE fromInteger #-}
+  x + y = wrapValue $ unwrapValue x + unwrapValue y
+  {-# INLINE (+) #-}
+  x - y = wrapValue $ unwrapValue x - unwrapValue y
+  {-# INLINE (-) #-}
+  x * y = wrapValue $ unwrapValue x * unwrapValue y
+  {-# INLINE (*) #-}
+  negate = wrapValue . negate . unwrapValue
+  {-# INLINE negate #-}
+  abs = wrapValue . abs . unwrapValue
+  {-# INLINE abs #-}
+  signum = wrapValue . signum . unwrapValue
+  {-# INLINE signum #-}
+
+instance Fractional (Value RealSort) where
+  fromRational = RealValue . fromRational
+  {-# INLINE fromRational #-}
+  (RealValue x) / (RealValue y) = RealValue $ x / y
+  {-# INLINE (/) #-}
+
+instance Boolean (Value BoolSort) where
+  bool = BoolValue
+  {-# INLINE bool #-}
+  (BoolValue x) && (BoolValue y) = BoolValue $ x && y
+  {-# INLINE (&&) #-}
+  (BoolValue x) || (BoolValue y) = BoolValue $ x || y
+  {-# INLINE (||) #-}
+  not (BoolValue x) = BoolValue $ not x
+  {-# INLINE not #-}
+  xor (BoolValue x) (BoolValue y) = BoolValue $ x `xor` y
+  {-# INLINE xor #-}
+
 -- | Unwraps a Haskell-value from the SMT-Context-'Value'.
 unwrapValue :: Value t -> HaskellType t
 unwrapValue (IntValue  v)   = v
@@ -86,7 +128,7 @@
 unwrapValue (BvValue   v)   = v
 unwrapValue (ArrayValue v)  = v
 unwrapValue (StringValue v) = v
-{-# INLINEABLE unwrapValue #-}
+{-# INLINE unwrapValue #-}
 
 -- | Wraps a Haskell-value into the SMT-Context-'Value'.
 wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
@@ -94,7 +136,7 @@
   SIntSort       -> IntValue
   SRealSort      -> RealValue
   SBoolSort      -> BoolValue
-  SBvSort _      -> BvValue
+  SBvSort _ _    -> BvValue
   SArraySort _ _ -> ArrayValue
   SStringSort    -> StringValue
-{-# INLINEABLE wrapValue #-}
+{-# INLINE wrapValue #-}