diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,16 @@
 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.3.0 _(2024-08-12)_
+
+### Added
+- Added full SMTLib2.6-standard support for sort String
+- Added module `Language.Hasmtlib.Lens` featuring `instance Plated (Expr t)` for rewriting
+
+### Changed
+- Export constructors of `Expr t`
+- `instance Show (Expr t)` now displays expressions in SMTLib2-Syntax
+
 ## v2.2.0 _(2024-08-09)_
 
 ### Added
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -59,12 +59,18 @@
 
 - [x] SMTLib2-Sorts in the Haskell-Type
   ```haskell
-    data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort
+    data SMTSort =
+        BoolSort
+      | IntSort
+      | RealSort
+      | BvSort 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
+- [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec, Array & String
 - [x] Type-level length-indexed Bitvectors for BitVec
   ```haskell
     bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
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.2.0
+version:               2.3.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.
@@ -14,7 +14,7 @@
 author:                Julian Bruder
 maintainer:            julian.bruder@outlook.com
 copyright:             © 2024 Julian Bruder
-category:              SMT
+category:              SMT, Logic
 build-type:            Simple
 extra-source-files:    README.md
 extra-doc-files:       CHANGELOG.md
@@ -26,6 +26,7 @@
   default-extensions:  DataKinds, GADTs, TypeFamilies, OverloadedStrings
 
   exposed-modules:     Language.Hasmtlib
+                     , Language.Hasmtlib.Lens
                      , Language.Hasmtlib.Codec
                      , Language.Hasmtlib.Iteable
                      , Language.Hasmtlib.Boolean
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -10,6 +10,7 @@
   , module Language.Hasmtlib.Type.SMTSort
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
+  , module Language.Hasmtlib.Lens
   , module Language.Hasmtlib.Integraled
   , module Language.Hasmtlib.Iteable
   , module Language.Hasmtlib.Boolean
@@ -38,6 +39,7 @@
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Lens
 import Language.Hasmtlib.Integraled
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Boolean
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
@@ -1,6 +1,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Language.Hasmtlib.Codec where
 
@@ -19,11 +20,13 @@
 import Data.IntMap as IM hiding (foldl)
 import Data.Dependent.Map as DMap
 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 GHC.Generics
+import GHC.TypeLits
 
 -- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' to it's type arguments.
 type family DefaultDecoded a :: Type where
@@ -35,13 +38,18 @@
   DefaultDecoded (t a b c) = t (Decoded a) (Decoded b) (Decoded c)
   DefaultDecoded (t a b) = t (Decoded a) (Decoded b)
   DefaultDecoded (t a) = t (Decoded a)
-  DefaultDecoded () = ()
+  DefaultDecoded x = TypeError (
+          Text "DefaultDecoded (" :<>: ShowType x :<>: Text ") is not allowed."
+    :$$:  Text "Try providing the associated Type Decoded (" :<>: ShowType x :<>: Text ") manually:"
+    :$$:  Text "instance Codec (" :<>: ShowType x :<>: Text ") where "
+    :$$:  Text "   type Decoded (" :<>: ShowType x :<>: Text ") = ... "
+    )
 
 -- | Lift values to SMT-Values or decode them.
 --
 --   You can derive an instance of this class if your type is 'Generic'.
 class Codec a where
-  -- | Resulting of decoding @a@
+  -- | Result of decoding @a@.
   type Decoded a :: Type
   type Decoded a = DefaultDecoded a
 
@@ -126,12 +134,29 @@
   decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
   decode sol (ArrSelect i arr)  = liftA2 arrSelect (decode sol i) (decode sol arr)
   decode sol (ArrStore i x arr) = liftM3 arrStore (decode sol i) (decode sol x) (decode sol arr)
+  decode sol (StrConcat x y)         = liftM2 (<>) (decode sol x) (decode sol y)
+  decode sol (StrLength x)           = toInteger . Text.length <$> decode sol x
+  decode sol (StrLT x y)             = liftM2 (<) (decode sol x) (decode sol y)
+  decode sol (StrLTHE x y)           = liftM2 (<=) (decode sol x) (decode sol y)
+  decode sol (StrAt x i)             = liftM2 (\x' i' -> Text.singleton $ Text.index x' (fromInteger i')) (decode sol x) (decode sol i)
+  decode sol (StrSubstring x i j)    = liftM3 (\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)       = liftM2 Text.isPrefixOf (decode sol x) (decode sol y)
+  decode sol (StrSuffixOf x y)       = liftM2 Text.isSuffixOf (decode sol x) (decode sol y)
+  decode sol (StrContains x y)       = liftM2 (flip Text.isInfixOf) (decode sol x) (decode sol y)
+  decode sol (StrIndexOf x y i)      = join $ liftM3 (\x' y' (fromInteger -> i') -> Text.findIndex ((y' ==) . Text.singleton) (Text.drop i' x') >>= Just . toInteger) (decode sol x) (decode sol y) (decode sol i)
+  decode sol (StrReplace src target replacement) = liftM3 (\src' target' replacement' -> replaceOne target' replacement' src') (decode sol target) (decode sol src) (decode sol replacement)
+    where
+      replaceOne pattern substitution text
+        | Text.null back = text
+        | otherwise = Text.concat [front, substitution, Text.drop (Text.length pattern) back]
+          where
+            (front, back) = Text.breakOn pattern text
+  decode sol (StrReplaceAll src target replacement) = liftM3 (\src' target' replacement' -> Text.replace target' replacement' src') (decode sol target) (decode sol src) (decode sol replacement)
   decode _ (ForAll _ _)         = Nothing
   decode _ (Exists _ _)         = Nothing
-
   encode = Constant . wrapValue
 
-instance Codec ()
+instance Codec () where type Decoded () = ()
 instance (Codec a, Codec b) => Codec (a,b)
 instance (Codec a, Codec b, Codec c) => Codec (a,b,c)
 instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d)
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -9,51 +9,59 @@
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Boolean
 import Data.Map hiding (toList)
-import Data.List (intercalate)
 import Data.Proxy
 import Data.Coerce
-import Data.Foldable (toList)
+import Data.String (IsString(..))
+import Data.Text (pack)
 import Data.ByteString.Builder
+import Data.ByteString.Lazy.UTF8 (toString)
 import qualified Data.Vector.Sized as V
 import Control.Lens
 import GHC.TypeLits
+import GHC.Generics
 
 -- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier.
 type role SMTVar phantom
-newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int } deriving (Show, Eq, Ord)
+newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int } deriving (Show, Eq, Ord, Generic)
 $(makeLenses ''SMTVar)
 
 -- | A wrapper for values of 'SMTSort's.
 data Value (t :: SMTSort) where
-  IntValue   :: HaskellType IntSort    -> Value IntSort
-  RealValue  :: HaskellType RealSort   -> Value RealSort
-  BoolValue  :: HaskellType BoolSort   -> Value BoolSort
-  BvValue    :: HaskellType (BvSort n) -> Value (BvSort n)
-  ArrayValue :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
+  IntValue    :: HaskellType IntSort    -> Value IntSort
+  RealValue   :: HaskellType RealSort   -> Value RealSort
+  BoolValue   :: HaskellType BoolSort   -> Value BoolSort
+  BvValue     :: HaskellType (BvSort n) -> Value (BvSort n)
+  ArrayValue  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
+  StringValue :: HaskellType StringSort -> Value StringSort
 
+deriving instance Eq (HaskellType t) => Eq (Value t)
+deriving instance Ord (HaskellType t) => Ord (Value t)
+
 -- | Unwrap a value from 'Value'.
 unwrapValue :: Value t -> HaskellType t
-unwrapValue (IntValue  v) = v
-unwrapValue (RealValue v) = v
-unwrapValue (BoolValue v) = v
-unwrapValue (BvValue   v) = v
-unwrapValue (ArrayValue v) = v
+unwrapValue (IntValue  v)   = v
+unwrapValue (RealValue v)   = v
+unwrapValue (BoolValue v)   = v
+unwrapValue (BvValue   v)   = v
+unwrapValue (ArrayValue v)  = v
+unwrapValue (StringValue v) = v
 {-# INLINEABLE unwrapValue #-}
 
 -- | Wrap a value into 'Value'.
 wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
 wrapValue = case sortSing @t of
-  SIntSort  -> IntValue
-  SRealSort -> RealValue
-  SBoolSort -> BoolValue
-  SBvSort _ -> BvValue
+  SIntSort       -> IntValue
+  SRealSort      -> RealValue
+  SBoolSort      -> BoolValue
+  SBvSort _      -> BvValue
   SArraySort _ _ -> ArrayValue
+  SStringSort    -> StringValue
 {-# INLINEABLE wrapValue #-}
 
 -- | An existential wrapper that hides some known 'SMTSort'.
 type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f
 
--- | A SMT expression.
+-- | Am SMT expression.
 --   For internal use only.
 --   For building expressions use the corresponding instances (Num, Boolean, ...).
 data Expr (t :: SMTSort) where
@@ -122,6 +130,19 @@
   ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => 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
+  StrSuffixOf   :: Expr StringSort -> Expr StringSort -> Expr BoolSort
+  StrContains   :: Expr StringSort -> Expr StringSort -> Expr BoolSort
+  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
   Exists    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
@@ -158,6 +179,16 @@
   minBound = Constant $ BvValue minBound
   maxBound = Constant $ BvValue maxBound
 
+instance Semigroup (Expr StringSort) where
+  (<>) = StrConcat
+
+instance Monoid (Expr StringSort) where
+  mempty = Constant $ StringValue mempty
+  mappend = (<>)
+
+instance IsString (Expr StringSort) where
+  fromString = Constant . StringValue . pack
+
 instance Render (SMTVar t) where
   render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)
   {-# INLINEABLE render #-}
@@ -176,6 +207,7 @@
       constRender v = "((as const " <> render (goSing arr) <> ") " <> render (wrapValue v) <> ")"
       goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)
       goSing _ = sortSing @(ArraySort k v)
+  render (StringValue x) = "\"" <> render x <> "\""
 
 instance KnownSMTSort t => Render (Expr t) where
   render (Var v)      = render v
@@ -243,6 +275,19 @@
   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)
+  render (StrSuffixOf x y)      = renderBinary "str.suffixof" (render x) (render y)
+  render (StrContains x y)      = renderBinary "str.contains" (render x) (render y)
+  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
 
@@ -257,70 +302,7 @@
 renderQuantifier _ Nothing _ = mempty
 
 instance Show (Value t) where
-  show (IntValue x)   = "IntValue "   ++ show x
-  show (RealValue x)  = "RealValue "  ++ show x
-  show (BoolValue x)  = "BoolValue "  ++ show x
-  show (BvValue x)    = "BvValue "    ++ show x
-  show (ArrayValue x) = "ArrValue: "  ++ show (render (ArrayValue x)) -- FIXME: This is bad but easy now
+  show = toString . toLazyByteString . render
 
-instance Show (Expr t) where
-  show (Var v)              = show v
-  show (Constant c)         = show c
-  show (Plus x y)           = "(" ++ show x ++ " + " ++ show y ++ ")"
-  show (Neg x)              = "(- " ++ show x ++ ")"
-  show (Mul x y)            = "(" ++ show x ++ " * " ++ show y ++ ")"
-  show (Abs x)              = "(abs " ++ show x ++ ")"
-  show (Mod x y)            = "(" ++ show x ++ " mod " ++ show y ++ ")"
-  show (IDiv x y)           = "(" ++ show x ++ " div " ++ show y ++ ")"
-  show (Div x y)            = "(" ++ show x ++ " / " ++ show y ++ ")"
-  show (LTH x y)            = "(" ++ show x ++ " < " ++ show y ++ ")"
-  show (LTHE x y)           = "(" ++ show x ++ " <= " ++ show y ++ ")"
-  show (EQU xs)             = "(= " ++ intercalate " " (show <$> toList xs) ++ ")"
-  show (Distinct xs)        = "(distinct " ++ intercalate " " (show <$> toList xs) ++ ")"
-  show (GTHE x y)           = "(" ++ show x ++ " >= " ++ show y ++ ")"
-  show (GTH x y)            = "(" ++ show x ++ " > " ++ show y ++ ")"
-  show (Not x)              = "(not " ++ show x ++ ")"
-  show (And x y)            = "(" ++ show x ++ " && " ++ show y ++ ")"
-  show (Or x y)             = "(" ++ show x ++ " || " ++ show y ++ ")"
-  show (Impl x y)           = "(" ++ show x ++ " ==> " ++ show y ++ ")"
-  show (Xor x y)            = "(" ++ show x ++ " xor " ++ show y ++ ")"
-  show Pi                   = "pi"
-  show (Sqrt x)             = "(sqrt "    ++ show x ++ ")"
-  show (Exp x)              = "(exp "     ++ show x ++ ")"
-  show (Sin x)              = "(sin "     ++ show x ++ ")"
-  show (Cos x)              = "(cos "     ++ show x ++ ")"
-  show (Tan x)              = "(tan "     ++ show x ++ ")"
-  show (Asin x)             = "(arcsin "  ++ show x ++ ")"
-  show (Acos x)             = "(arccos "  ++ show x ++ ")"
-  show (Atan x)             = "(arctan "  ++ show x ++ ")"
-  show (ToReal x)           = "(to_real " ++ show x ++ ")"
-  show (ToInt x)            = "(to_int "  ++ show x ++ ")"
-  show (IsInt x)            = "(is_int "  ++ show x ++ ")"
-  show (Ite p t f)          = "(ite " ++ show p ++ " " ++ show t ++ " " ++ show f ++ ")"
-  show (BvNot x)            = "(not "  ++ show x ++ ")"
-  show (BvAnd x y)          = "(" ++ show x ++ " && " ++ show y ++ ")"
-  show (BvOr x y)           = "(" ++ show x ++ " || " ++ show y ++ ")"
-  show (BvXor x y)          = "(" ++ show x ++ " xor " ++ show y ++ ")"
-  show (BvNand x y)         = "(" ++ show x ++ " nand " ++ show y ++ ")"
-  show (BvNor x y)          = "(" ++ show x ++ " nor " ++ show y ++ ")"
-  show (BvNeg x)            = "(- " ++ show x ++ ")"
-  show (BvAdd x y)          = "(" ++ show x ++ " + " ++ show y ++ ")"
-  show (BvSub x y)          = "(" ++ show x ++ " - " ++ show y ++ ")"
-  show (BvMul x y)          = "(" ++ show x ++ " * " ++ show y ++ ")"
-  show (BvuDiv x y)         = "(" ++ show x ++ " udiv " ++ show y ++ ")"
-  show (BvuRem x y)         = "(" ++ show x ++ " urem " ++ show y ++ ")"
-  show (BvShL x y)          = "(" ++ show x ++ " bvshl " ++ show y ++ ")"
-  show (BvLShR x y)         = "(" ++ show x ++ " bvlshr " ++ show y ++ ")"
-  show (BvConcat x y)       = "(" ++ show x ++ " bvconcat " ++ show y ++ ")"
-  show (BvRotL i x)         = "(" ++ show x ++ " bvrotl " ++ show (natVal i) ++ ")"
-  show (BvRotR i x)         = "(" ++ show x ++ " bvrotr " ++ show (natVal i) ++ ")"
-  show (BvuLT x y)          = "(" ++ show x ++ " bvult " ++ show y ++ ")"
-  show (BvuLTHE x y)        = "(" ++ show x ++ " bvule " ++ show y ++ ")"
-  show (BvuGTHE x y)        = "(" ++ show x ++ " bvuge " ++ show y ++ ")"
-  show (BvuGT x y)          = "(" ++ show x ++ " bvugt " ++ show y ++ ")"
-  show (ForAll (Just qv) f) = "(forall " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
-  show (ForAll Nothing f)   = "(forall var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
-  show (ArrSelect i arr)    = "(select " ++ show i ++ " " ++ show arr ++ ")"
-  show (ArrStore i x arr)   = "(select " ++ show i ++ " " ++ show x ++ " " ++ show arr ++ ")"
-  show (Exists (Just qv) f) = "(exists " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
-  show (Exists Nothing f)   = "(exists var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
+instance KnownSMTSort t => Show (Expr t) where
+  show = toString . toLazyByteString . render
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
@@ -16,14 +16,17 @@
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Type.Expr
 import Data.Bit
 import Data.Coerce
 import Data.Proxy
 import Data.Ratio ((%))
 import Data.ByteString
 import Data.ByteString.Builder
-import Data.Attoparsec.ByteString hiding (Result, skipWhile)
+import Data.Attoparsec.ByteString hiding (Result, skipWhile, takeTill)
 import Data.Attoparsec.ByteString.Char8 hiding (Result)
+import Data.Text.Encoding (decodeUtf8)
+import qualified Data.Text as Text
 import Control.Applicative
 import Control.Lens hiding (op)
 import GHC.TypeNats
@@ -83,6 +86,7 @@
         <|> (string "Real" *> pure (SomeSMTSort SRealSort))
         <|> parseSomeBitVecSort
         <|> parseSomeArraySort
+        <|> (string "String" *> pure (SomeSMTSort SStringSort))
 {-# INLINEABLE parseSomeSort #-}
 
 parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
@@ -115,19 +119,19 @@
 
 -- TODO: Add parseSelect
 parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
-parseExpr = var <|> constantExpr <|> smtIte
+parseExpr = var <|> constantExpr <|> ternary "ite" (ite @(Expr BoolSort))
         <|> case sortSing @t of
               SIntSort  -> unary "abs" abs <|> unary  "-" negate
                       <|> nary "+" sum  <|> binary "-" (-) <|> nary "*" product <|> binary "mod" Mod
-                      <|> toIntFun
+                      <|> unary "to_int" toIntSort <|> unary "str.len" strLength
+                      <|> ternary "str.indexof" strIndexOf
               SRealSort -> unary "abs" abs <|> unary  "-" negate
                       <|> nary "+" sum  <|> binary "-" (-) <|> nary "*" product <|> binary "/" (/)
-                      <|> toRealFun
+                      <|> unary "to_real" toRealSort
                       <|> smtPi <|> unary "sqrt" sqrt <|> unary "exp" exp
                       <|> unary "sin" sin <|> unary "cos" cos <|> unary "tan" tan
                       <|> unary "arcsin" asin <|> unary "arccos" acos <|> unary "arctan" atan
-              SBoolSort -> isIntFun
-                      <|> unary "not" not
+              SBoolSort -> unary "not" not
                       <|> nary "and" and  <|> nary "or" or <|> binary "=>" (==>) <|> binary "xor" xor
                       <|> binary @IntSort  "=" (===) <|> binary @IntSort  "distinct" (/==)
                       <|> binary @RealSort "=" (===) <|> binary @RealSort "distinct" (/==)
@@ -136,6 +140,10 @@
                       <|> binary @IntSort ">=" (>=?) <|> binary @IntSort ">" (>?)
                       <|> binary @RealSort "<" (<?) <|> binary @RealSort "<=" (<=?)
                       <|> binary @RealSort ">=" (>=?) <|> binary @RealSort ">" (>?)
+                      <|> binary @StringSort "str.<" (<?) <|> binary @StringSort "str.<=" (<=?)
+                      <|> unary "is_int" isIntSort
+                      <|> binary "str.prefixof" strPrefixOf <|> binary "str.suffixof" strSuffixOf
+                      <|> binary "str.contains" strContains
                       -- TODO: Add compare ops for all (?) bv-sorts
               SBvSort _ -> unary "bvnot" not
                       <|> binary "bvand" (&&)  <|> binary "bvor" (||) <|> binary "bvxor" xor <|> binary "bvnand" BvNand <|> binary "bvnor" BvNor
@@ -143,14 +151,15 @@
                       <|> binary "bvadd" (+)  <|> binary "bvsub" (-) <|> binary "bvmul" (*)
                       <|> binary "bvudiv" BvuDiv <|> binary "bvurem" BvuRem
                       <|> binary "bvshl" BvShL <|> binary "bvlshr" BvLShR
-              SArraySort _ _ -> parseStore
+              SArraySort _ _ -> ternary "store" ArrStore
                       -- TODO: Add compare ops for all (?) array-sorts
+              SStringSort -> binary "str.++" (<>) <|> binary "str.at" strAt <|> ternary "str.substr" StrSubstring
+                      <|> ternary "str.replace" strReplace <|> ternary "str.replace_all" strReplaceAll
 
 var :: Parser (Expr t)
 var = do
   _     <- string "var_"
   vId <- decimal @Int
-
   return $ Var $ coerce vId
 {-# INLINE var #-}
 
@@ -161,7 +170,8 @@
   SBoolSort -> parseBool
   SBvSort p -> anyBitvector p
   SArraySort k v -> constArray k v
-{-# INLINE constant #-}
+  SStringSort -> parseSmtString
+{-# INLINEABLE constant #-}
 
 constantExpr :: forall t. KnownSMTSort t => Parser (Expr t)
 constantExpr = Constant . wrapValue <$> constant @t
@@ -210,29 +220,12 @@
   return $ asConst constVal
 {-# INLINEABLE constArray #-}
 
-parseSelect :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Parser (Expr v)
-parseSelect _ = do
-  _ <- char '(' >> skipSpace
-  _ <- string "select" >> skipSpace
-  arr <- parseExpr @(ArraySort k v)
-  _ <- skipSpace
-  i <- parseExpr @k
-  _ <- skipSpace >> char ')'
-
-  return $ ArrSelect arr i
-
-parseStore :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Parser (Expr (ArraySort k v))
-parseStore = do
-  _ <- char '(' >> skipSpace
-  _ <- string "store" >> skipSpace
-  arr <- parseExpr @(ArraySort k v)
-  _ <- skipSpace
-  i <- parseExpr @k
-  _ <- skipSpace
-  x <- parseExpr @v
-  _ <- skipSpace >> char ')'
-
-  return $ ArrStore arr i x
+parseSmtString :: Parser Text.Text
+parseSmtString = do
+  _ <- char '"'
+  s <- decodeUtf8 <$> takeTill (== '"')
+  _ <- char '"'
+  return s
 
 unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
 unary opStr op = do
@@ -244,7 +237,7 @@
   return $ op val
 {-# INLINE unary #-}
 
-binary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
+binary :: forall t u r. (KnownSMTSort t, KnownSMTSort u) => ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
 binary opStr op = do
   _ <- char '(' >> skipSpace
   _ <- string opStr >> skipSpace
@@ -255,6 +248,19 @@
   return $ l `op` r
 {-# INLINE binary #-}
 
+ternary :: forall t u v r. (KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) => ByteString -> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
+ternary opStr op = do
+  _ <- char '(' >> skipSpace
+  _ <- string opStr >> skipSpace
+  l <- parseExpr
+  _ <- skipSpace
+  m <- parseExpr
+  _ <- skipSpace
+  r <- parseExpr
+  _ <- skipSpace >> char ')'
+  return $ op l m r
+{-# INLINE ternary #-}
+
 nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
 nary opStr op = do
   _    <- char '(' >> skipSpace
@@ -267,50 +273,6 @@
 smtPi :: Parser (Expr RealSort)
 smtPi = string "real.pi" *> return pi
 {-# INLINE smtPi #-}
-
-toRealFun :: Parser (Expr RealSort)
-toRealFun = do
-  _ <- char '(' >> skipSpace
-  _ <- string "to_real" >> skipSpace
-  val <- parseExpr
-  _ <- skipSpace >> char ')'
-
-  return $ ToReal val
-{-# INLINEABLE toRealFun #-}
-
-toIntFun :: Parser (Expr IntSort)
-toIntFun = do
-  _ <- char '(' >> skipSpace
-  _ <- string "to_int" >> skipSpace
-  val <- parseExpr
-  _ <- skipSpace >> char ')'
-
-  return $ ToInt val
-{-# INLINEABLE toIntFun #-}
-
-isIntFun :: Parser (Expr BoolSort)
-isIntFun = do
-  _ <- char '(' >> skipSpace
-  _ <- string "is_int" >> skipSpace
-  val <- parseExpr
-  _ <- skipSpace >> char ')'
-
-  return $ IsInt val
-{-# INLINEABLE isIntFun #-}
-
-smtIte :: forall t. KnownSMTSort t => Parser (Expr t)
-smtIte = do
-  _ <- char '(' >> skipSpace
-  _ <- string "ite" >> skipSpace
-  p <- parseExpr @BoolSort
-  _ <- skipSpace
-  t <- parseExpr
-  _ <- skipSpace
-  f <- parseExpr
-  _ <- skipSpace >> char ')'
-
-  return $ ite p t f
-{-# INLINEABLE smtIte #-}
 
 anyValue :: Num a => Parser a -> Parser a
 anyValue p = negativeValue p <|> p
diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs
--- a/src/Language/Hasmtlib/Internal/Render.hs
+++ b/src/Language/Hasmtlib/Internal/Render.hs
@@ -3,6 +3,8 @@
 import Data.ByteString.Builder
 import Data.Foldable (foldl')
 import Data.Sequence
+import qualified Data.Text as Text
+import qualified Data.Text.Encoding as Text.Enc
 import GHC.TypeNats
 
 -- | Render values to their SMTLib2-Lisp form, represented as 'Builder'.
@@ -39,6 +41,10 @@
 
 instance Render Builder where
   render = id
+  {-# INLINE render #-}
+
+instance Render Text.Text where
+  render = Text.Enc.encodeUtf8Builder
   {-# INLINE render #-}
 
 renderUnary :: Render a => Builder -> a -> Builder
diff --git a/src/Language/Hasmtlib/Lens.hs b/src/Language/Hasmtlib/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Lens.hs
@@ -0,0 +1,211 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Language.Hasmtlib.Lens where
+
+import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Type.SMTSort
+import Language.Hasmtlib.Equatable
+import Language.Hasmtlib.Orderable
+import Language.Hasmtlib.Iteable
+import Data.GADT.Compare
+import Control.Lens
+
+type instance Index   (Expr StringSort) = Expr IntSort
+type instance IxValue (Expr StringSort) = Expr StringSort
+
+instance Ixed (Expr StringSort) where
+  ix i f s = f (strAt s i) <&> \a ->
+    let l = strSubstring a 0 i
+        r = strSubstring a i (strLength a)
+     in l <> strReplace r (strAt a i) s
+
+instance AsEmpty (Expr StringSort) where
+  _Empty = prism'
+    (const mempty)
+    (\s -> ite (s === mempty) (Just ()) Nothing)
+
+instance Prefixed (Expr StringSort) where
+  prefixed p = prism'
+    (p <>)
+    (\s -> ite (p `strPrefixOf` s) (Just $ strReplace s p mempty) Nothing)
+
+instance Suffixed (Expr StringSort) where
+  suffixed qs = prism'
+    (<> qs)
+    (\s -> ite (qs `strSuffixOf` s) (Just $ strSubstring s 0 (strLength s - strLength qs)) Nothing)
+
+instance Cons (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where
+  _Cons = prism'
+    (uncurry (<>))
+    (\s -> ite (strLength s >? 0) (Just (strAt s 0, strSubstring s 1 (strLength s))) Nothing)
+
+instance Snoc (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where
+  _Snoc = prism'
+    (uncurry (<>))
+    (\s -> ite (strLength s >? 0) (Just (strSubstring s 0 (strLength s - 1), strAt s (strLength s - 1))) Nothing)
+
+type instance Index   (Expr (ArraySort k v)) = Expr k
+type instance IxValue (Expr (ArraySort k v)) = Expr v
+
+instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Ixed (Expr (ArraySort k v)) where
+  ix i f arr = f (select arr i) <&> store arr i
+
+-- | **Caution for quantified expressions:** 'plate-function' @f@ will only be applied if quantification already has taken place.(&&)
+--   Therefore make sure 'quantify' has been run before.
+--   Otherwise the quantified expression and therefore all it's sub-expressions will not have @f@ applied.
+instance KnownSMTSort t => Plated (Expr t) where
+  plate _ expr@(Var _)            = pure expr
+  plate _ expr@(Constant _)       = pure expr
+  plate f (Plus x y)              = Plus <$> f x <*> f y
+  plate f (Neg x)                 = Neg <$> f x
+  plate f (Mul x y)               = Mul <$> f x <*> f y
+  plate f (Abs x)                 = Abs <$> f x
+  plate f (Mod x y)               = Mod <$> f x <*> f y
+  plate f (IDiv x y)              = IDiv <$> f x <*> f y
+  plate f (Div x y)               = Div <$> f x <*> f y
+  plate f (LTH x y)               = LTH <$> somePlate f x <*> somePlate f y
+  plate f (LTHE x y)              = LTHE <$> somePlate f x <*> somePlate f y
+  plate f (EQU xs)                = EQU <$> traverse (somePlate f) xs
+  plate f (Distinct xs)           = Distinct <$> traverse (somePlate f) xs
+  plate f (GTHE x y)              = GTHE <$> somePlate f x <*> somePlate f y
+  plate f (GTH x y)               = GTH <$> somePlate f x <*> somePlate f y
+  plate f (Not x)                 = Not <$> somePlate f x
+  plate f (And x y)               = And <$> somePlate f x <*> somePlate f y
+  plate f (Or x y)                = Or <$> somePlate f x <*> somePlate f y
+  plate f (Impl x y)              = Impl <$> somePlate f x <*> somePlate f y
+  plate f (Xor x y)               = Xor <$> somePlate f x <*> somePlate f y
+  plate _ Pi                      = pure Pi
+  plate f (Sqrt x)                = Sqrt <$> f x
+  plate f (Exp x)                 = Exp <$> f x
+  plate f (Sin x)                 = Sin <$> f x
+  plate f (Cos x)                 = Cos <$> f x
+  plate f (Tan x)                 = Tan <$> f x
+  plate f (Asin x)                = Asin <$> f x
+  plate f (Acos x)                = Acos <$> f x
+  plate f (Atan x)                = Atan <$> f x
+  plate f (ToReal x)              = ToReal <$> somePlate f x
+  plate f (ToInt x)               = ToInt <$> somePlate f x
+  plate f (IsInt x)               = IsInt <$> somePlate f x
+  plate f (Ite p t n)             = Ite <$> somePlate f p <*> f t <*> f n
+  plate f (BvNot x)               = BvNot <$> f x
+  plate f (BvAnd x y)             = BvAnd <$> f x <*> f y
+  plate f (BvOr x y)              = BvOr <$> f x <*> f y
+  plate f (BvXor x y)             = BvXor <$> f x <*> f y
+  plate f (BvNand x y)            = BvNand <$> f x <*> f y
+  plate f (BvNor x y)             = BvNor <$> f x <*> f y
+  plate f (BvNeg x)               = BvNeg <$> f x
+  plate f (BvAdd x y)             = BvAdd <$> f x <*> f y
+  plate f (BvSub x y)             = BvSub <$> f x <*> f y
+  plate f (BvMul x y)             = BvMul <$> f x <*> f y
+  plate f (BvuDiv x y)            = BvuDiv <$> f x <*> f y
+  plate f (BvuRem x y)            = BvuRem <$> f x <*> f y
+  plate f (BvShL x y)             = BvShL <$> f x <*> f y
+  plate f (BvLShR x y)            = BvLShR <$> f x <*> f y
+  plate f (BvConcat x y)          = BvConcat <$> somePlate f x <*> somePlate f y
+  plate f (BvRotL i x)            = BvRotL i <$> f x
+  plate f (BvRotR i x)            = BvRotR i <$> f x
+  plate f (BvuLT x y)             = BvuLT <$> somePlate f x <*> somePlate f y
+  plate f (BvuLTHE x y)           = BvuLTHE <$> somePlate f x <*> somePlate f y
+  plate f (BvuGTHE x y)           = BvuGTHE <$> somePlate f x <*> somePlate f y
+  plate f (BvuGT x y)             = BvuGT <$> somePlate f x <*> somePlate f y
+  plate f (ArrSelect i arr)       = ArrSelect i <$> somePlate f arr
+  plate f (ArrStore i x arr)      = ArrStore i <$> somePlate f x <*> somePlate f arr
+  plate f (StrConcat x y)         = StrConcat <$> f x <*> f y
+  plate f (StrLength x)           = StrLength <$> somePlate f x
+  plate f (StrLT x y)             = StrLT <$> somePlate f x <*> somePlate f y
+  plate f (StrLTHE x y)           = StrLTHE <$> somePlate f x <*> somePlate f y
+  plate f (StrAt x i)             = StrAt <$> f x <*> somePlate f i
+  plate f (StrSubstring x i j)    = StrSubstring <$> f x <*> somePlate f i <*> somePlate f j
+  plate f (StrPrefixOf x y)       = StrPrefixOf <$> somePlate f x <*> somePlate f y
+  plate f (StrSuffixOf x y)       = StrSuffixOf <$> somePlate f x <*> somePlate f y
+  plate f (StrContains x y)       = StrContains <$> somePlate f x <*> somePlate f y
+  plate f (StrIndexOf x y i)      = StrIndexOf <$> somePlate f x <*> somePlate f y <*> f i
+  plate f (StrReplace x y y')     = StrReplace <$> f x <*> f y <*> f y'
+  plate f (StrReplaceAll x y y')  = StrReplaceAll <$> f x <*> f y <*> f y'
+  plate f (ForAll (Just qv) expr) = ForAll (Just qv) . const <$> somePlate f (expr (Var qv))
+  plate _ (ForAll Nothing expr)   = pure $ ForAll Nothing expr
+  plate f (Exists (Just qv) expr) = Exists (Just qv) . const <$> somePlate f (expr (Var qv))
+  plate _ (Exists Nothing expr)   = pure $ Exists Nothing expr
+
+-- | Apply the 'plate'-function @f@ for given 'Expr' @expr@ if possible.
+--   Otherwise try to apply @f@ for the children of @expr@.
+--   **Caution for quantified expressions:** 'plate-function' @f@ will only be applied if quantification already has taken place.(&&)
+--   Therefore make sure 'quantify' has been run before.
+--   Otherwise the quantified expression and therefore all it's sub-expressions will not have @f@ applied.
+somePlate :: forall t f. (KnownSMTSort t, Applicative f) => (Expr t -> f (Expr t)) -> (forall s. KnownSMTSort s => Expr s -> f (Expr s))
+somePlate f expr = case geq (sortSing @t) (sortSing' expr) of
+  Just Refl -> f expr
+  Nothing   -> case expr of
+    Var _                -> pure expr
+    Constant _           -> pure expr
+    Plus x y             -> Plus <$> somePlate f x <*> somePlate f y
+    Neg x                -> Neg  <$> somePlate f x
+    Mul x y              -> Mul  <$> somePlate f x <*> somePlate f y
+    Abs x                -> Abs  <$> somePlate f x
+    Mod x y              -> Mod  <$> somePlate f x <*> somePlate f y
+    IDiv x y             -> IDiv <$> somePlate f x <*> somePlate f y
+    Div x y              -> Div  <$> somePlate f x <*> somePlate f y
+    LTH x y              -> LTH  <$> somePlate f x <*> somePlate f y
+    LTHE x y             -> LTHE <$> somePlate f x <*> somePlate f y
+    EQU xs               -> EQU  <$> traverse (somePlate f) xs
+    Distinct xs          -> Distinct <$> traverse (somePlate f) xs
+    GTHE x y             -> GTHE <$> somePlate f x <*> somePlate f y
+    GTH x y              -> GTH  <$> somePlate f x <*> somePlate f y
+    Not x                -> Not  <$> somePlate f x
+    And x y              -> And  <$> somePlate f x <*> somePlate f y
+    Or x y               -> Or   <$> somePlate f x <*> somePlate f y
+    Impl x y             -> Impl <$> somePlate f x <*> somePlate f y
+    Xor x y              -> Xor  <$> somePlate f x <*> somePlate f y
+    Pi                   -> pure Pi
+    Sqrt x               -> Sqrt <$> somePlate f x
+    Exp x                -> Exp  <$> somePlate f x
+    Sin x                -> Sin  <$> somePlate f x
+    Cos x                -> Cos  <$> somePlate f x
+    Tan x                -> Tan  <$> somePlate f x
+    Asin x               -> Asin <$> somePlate f x
+    Acos x               -> Acos <$> somePlate f x
+    Atan x               -> Atan <$> somePlate f x
+    ToReal x             -> ToReal <$> somePlate f x
+    ToInt x              -> ToInt  <$> somePlate f x
+    IsInt x              -> IsInt  <$> somePlate f x
+    Ite p t n            -> Ite    <$> somePlate f p <*> somePlate f t <*> somePlate f n
+    BvNot x              -> BvNot  <$> somePlate f x
+    BvAnd x y            -> BvAnd  <$> somePlate f x <*> somePlate f y
+    BvOr x y             -> BvOr   <$> somePlate f x <*> somePlate f y
+    BvXor x y            -> BvXor  <$> somePlate f x <*> somePlate f y
+    BvNand x y           -> BvNand <$> somePlate f x <*> somePlate f y
+    BvNor x y            -> BvNor  <$> somePlate f x <*> somePlate f y
+    BvNeg x              -> BvNeg  <$> somePlate f x
+    BvAdd x y            -> BvAdd  <$> somePlate f x <*> somePlate f y
+    BvSub x y            -> BvSub  <$> somePlate f x <*> somePlate f y
+    BvMul x y            -> BvMul  <$> somePlate f x <*> somePlate f y
+    BvuDiv x y           -> BvuDiv <$> somePlate f x <*> somePlate f y
+    BvuRem x y           -> BvuRem <$> somePlate f x <*> somePlate f y
+    BvShL x y            -> BvShL  <$> somePlate f x <*> somePlate f y
+    BvLShR x y           -> BvLShR <$> somePlate f x <*> somePlate f y
+    BvConcat x y         -> BvConcat <$> somePlate f x <*> somePlate f y
+    BvRotL i x           -> BvRotL i <$> somePlate f x
+    BvRotR i x           -> BvRotR i <$> somePlate f x
+    BvuLT x y            -> BvuLT    <$> somePlate f x <*> somePlate f y
+    BvuLTHE x y          -> BvuLTHE  <$> somePlate f x <*> somePlate f y
+    BvuGTHE x y          -> BvuGTHE  <$> somePlate f x <*> somePlate f y
+    BvuGT x y            -> BvuGT    <$> somePlate f x <*> somePlate f y
+    ArrSelect i arr      -> ArrSelect i   <$> somePlate f arr
+    ArrStore i x arr     -> ArrStore i    <$> somePlate f x <*> somePlate f arr
+    StrConcat x y        -> StrConcat     <$> somePlate f x <*> somePlate f y
+    StrLength x          -> StrLength     <$> somePlate f x
+    StrLT x y            -> StrLT         <$> somePlate f x <*> somePlate f y
+    StrLTHE x y          -> StrLTHE       <$> somePlate f x <*> somePlate f y
+    StrAt x i            -> StrAt         <$> somePlate f x <*> somePlate f i
+    StrSubstring x i j   -> StrSubstring  <$> somePlate f x <*> somePlate f i <*> somePlate f j
+    StrPrefixOf x y      -> StrPrefixOf   <$> somePlate f x <*> somePlate f y
+    StrSuffixOf x y      -> StrSuffixOf   <$> somePlate f x <*> somePlate f y
+    StrContains x y      -> StrContains   <$> somePlate f x <*> somePlate f y
+    StrIndexOf x y i     -> StrIndexOf    <$> somePlate f x <*> somePlate f y <*> somePlate f i
+    StrReplace x y y'    -> StrReplace    <$> somePlate f x <*> somePlate f y <*> somePlate f y'
+    StrReplaceAll x y y' -> StrReplaceAll <$> somePlate f x <*> somePlate f y <*> somePlate f y'
+    ForAll (Just qv) qexpr -> ForAll (Just qv) . const <$> somePlate f (qexpr (Var qv))
+    ForAll Nothing qexpr   -> pure $ ForAll Nothing qexpr
+    Exists (Just qv) qexpr -> Exists (Just qv) . const <$> somePlate f (qexpr (Var qv))
+    Exists Nothing qexpr   -> pure $ Exists Nothing qexpr
diff --git a/src/Language/Hasmtlib/Orderable.hs b/src/Language/Hasmtlib/Orderable.hs
--- a/src/Language/Hasmtlib/Orderable.hs
+++ b/src/Language/Hasmtlib/Orderable.hs
@@ -85,6 +85,13 @@
   (>?)     = BvuGT
   {-# 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
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
@@ -4,12 +4,13 @@
 module Language.Hasmtlib.Type.Expr
  ( SMTVar(..), varId
  , Value(..), unwrapValue, wrapValue
- , Expr
+ , Expr(..)
  , equal, distinct
  , bvShL, bvLShR, bvConcat, bvRotL, bvRotR
  , toIntSort, toRealSort, isIntSort
  , for_all , exists
  , select, store
+ , strLength, strAt, strSubstring, strPrefixOf, strSuffixOf, strContains, strIndexOf, strReplace, strReplaceAll
  )
 where
 
@@ -118,3 +119,56 @@
 -- | Checks whether an expression of type 'RealSort' may be safely converted to type 'IntSort'.
 isIntSort :: Expr RealSort -> Expr BoolSort
 isIntSort = IsInt
+
+-- | Length of a string.
+strLength :: Expr StringSort -> Expr IntSort
+strLength = StrLength
+
+-- | Singleton string containing a character at given position
+--   or empty string when position is out of range.
+--   The leftmost position is 0.
+strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort
+strAt = StrAt
+
+-- | @(strSubstring s i n)@ evaluates to the longest (unscattered) substring
+--   of @s@ of length at most @n@ starting at position @i@.
+--   It evaluates to the empty string if @n@ is negative or @i@ is not in
+--   the interval @[0,l-1]@ where @l@ is the length of @s@.
+strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
+strSubstring = StrSubstring
+
+-- | First string is a prefix of second one.
+--   @(str.prefixof s t)@ is @true@ iff @s@ is a prefix of @t@.
+strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
+strPrefixOf = StrPrefixOf
+
+-- | First string is a suffix of second one.
+--   @(str.suffixof s t)@ is @true@ iff @s@ is a suffix of @t@.
+strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
+strSuffixOf = StrSuffixOf
+
+-- | First string contains second one
+--   @(str.contains s t)@ iff @s@ contains @t@.
+strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort
+strContains = StrContains
+
+-- | Index of first occurrence of second string in first one starting at the position specified by the third argument.
+--   @(str.indexof s t i)@, with @0 <= i <= |s|@ is the position of the first
+--   occurrence of @t@ in @s@ at or after position @i@, if any.
+--   Otherwise, it is @-1@. Note that the result is @i@ whenever @i@ is within
+--   the range @[0, |s|]@ and @t@ is empty.
+strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
+strIndexOf = StrIndexOf
+
+-- | @(str.replace s t t')@ is the string obtained by replacing the first
+--   occurrence of @t@ in @s@, if any, by @t'@. Note that if @t@ is empty, the
+--   result is to prepend @t'@ to @s@; also, if @t@ does not occur in @s@ then
+--   the result is @s@.
+strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
+strReplace = StrReplace
+
+-- | @(str.replace_all s t t’)@ is @s@ if @t@ is the empty string. Otherwise, it
+--   is the string obtained from @s@ by replacing all occurrences of @t@ in @s@
+--   by @t’@, starting with the first occurrence and proceeding in left-to-right order.
+strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
+strReplaceAll = StrReplaceAll
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
@@ -10,6 +10,7 @@
 import Data.Kind
 import Data.Proxy
 import Data.ByteString.Builder
+import qualified Data.Text as Text
 import Control.Lens
 import GHC.TypeLits
 
@@ -20,6 +21,7 @@
   | RealSort                      -- ^ Sort of Real
   | BvSort Nat                    -- ^ Sort of BitVec with length n
   | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v
+  | StringSort                    -- ^ Sort of String
 
 -- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.
 type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
@@ -28,14 +30,16 @@
   HaskellType BoolSort        = Bool
   HaskellType (BvSort n)      = Bitvec n
   HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)
+  HaskellType StringSort      = Text.Text
 
 -- | Singleton for 'SMTSort'.
 data SSMTSort (t :: SMTSort) where
-  SIntSort   :: SSMTSort IntSort
-  SRealSort  :: SSMTSort RealSort
-  SBoolSort  :: SSMTSort BoolSort
-  SBvSort    :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
-  SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
+  SIntSort    :: SSMTSort IntSort
+  SRealSort   :: SSMTSort RealSort
+  SBoolSort   :: SSMTSort BoolSort
+  SBvSort     :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
+  SArraySort  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
+  SStringSort :: SSMTSort StringSort
 
 deriving instance Show (SSMTSort t)
 deriving instance Eq   (SSMTSort t)
@@ -46,8 +50,14 @@
   geq SRealSort SRealSort     = Just Refl
   geq SBoolSort SBoolSort     = Just Refl
   geq (SBvSort n) (SBvSort m) = case sameNat n m 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
+      Nothing -> Nothing
+      Just Refl -> Just Refl
+  geq SStringSort SStringSort = Just Refl
   geq _ _                     = Nothing
 
 instance GCompare SSMTSort where
@@ -65,6 +75,7 @@
       GEQ -> GEQ
       GGT -> GGT
     GGT -> GGT
+  gcompare SStringSort SStringSort = GEQ
   gcompare SBoolSort _        = GLT
   gcompare _ SBoolSort        = GGT
   gcompare SIntSort _         = GLT
@@ -73,6 +84,8 @@
   gcompare _ SRealSort        = GGT
   gcompare (SArraySort _ _) _ = GLT
   gcompare _ (SArraySort _ _) = GGT
+  gcompare SStringSort _      = GLT
+  gcompare _ SStringSort      = GGT
 
 -- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.
 class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t
@@ -82,6 +95,7 @@
 instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)
 instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where
    sortSing = SArraySort (Proxy @k) (Proxy @v)
+instance KnownSMTSort StringSort                 where sortSing = SStringSort
 
 -- | Wrapper for 'sortSing' which takes a 'Proxy'
 sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
@@ -108,4 +122,5 @@
   render SRealSort   = "Real"
   render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
   render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)
+  render SStringSort   = "String"
   {-# INLINEABLE render #-}