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:               1.0.2
+version:               1.1.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.
@@ -47,6 +47,7 @@
                      , Language.Hasmtlib.Type.Solution
                      , Language.Hasmtlib.Type.Solver
                      , Language.Hasmtlib.Type.Option
+                     , Language.Hasmtlib.Type.ArrayMap
 
   other-modules:       Language.Hasmtlib.Internal.Expr
                      , Language.Hasmtlib.Internal.Expr.Num
@@ -55,12 +56,14 @@
                      , base                         >= 4.17.2 && < 5
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1
+                     , dependent-map                >= 0.4    && < 1
                      , mtl                          >= 2.2.2  && < 3
                      , text                         >= 2.0.2  && < 3
                      , data-default                 >= 0.7.1  && < 1
                      , lens                         >= 5      && < 6
                      , smtlib-backends              >= 0.4    && < 1
                      , smtlib-backends-process      >= 0.3    && < 1
+                     , some                         >= 1.0.6  && < 1.1
                      , utf8-string                  >= 1.0.2  && < 2
                      , bitvec                       >= 1.1.5  && < 2
                      , finite-typelits              >= 0.1.0  && < 1
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -7,6 +7,7 @@
   , module Language.Hasmtlib.Type.Solver
   , module Language.Hasmtlib.Type.Option
   , module Language.Hasmtlib.Type.Solution
+  , module Language.Hasmtlib.Type.ArrayMap
   , module Language.Hasmtlib.Integraled
   , module Language.Hasmtlib.Iteable
   , module Language.Hasmtlib.Boolean
@@ -29,6 +30,7 @@
 import Language.Hasmtlib.Type.Solver
 import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Type.ArrayMap
 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
@@ -8,17 +8,16 @@
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Boolean
 import Data.Kind
 import Data.Coerce
-import Data.Proxy
 import Data.Map (Map)
 import Data.Sequence (Seq)
 import Data.IntMap as IM
+import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
-import qualified Data.Vector.Unboxed.Sized as V
 import Control.Monad
-import GHC.TypeNats
 
 -- | Compute the default 'Decoded' 'Type' for every functor-wrapper.
 --   Useful for instances using default signatures.
@@ -43,57 +42,42 @@
 -- | Decode and evaluate expressions
 instance KnownSMTSort t => Codec (Expr t) where
   type Decoded (Expr t) = HaskellType t
-  decode sol (Var var)    = do
-    someSol <- IM.lookup (coerce var) sol
-    case sortSing @t of
-      SIntSort   -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (IntValue v))  -> Just v
-                    _                                            -> Nothing
-      SRealSort  -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (RealValue v)) -> Just v
-                    _                                            -> Nothing
-      SBoolSort  -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (BoolValue v)) -> Just v
-                    _                                            -> Nothing
-      SBvSort p  -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (BvValue v))   -> goN p v
-                    _                                            -> Nothing
-        where
-          goN :: forall n m. KnownNat n => Proxy n -> Bitvec m -> Maybe (Bitvec n)
-          goN _ = coerce . V.toSized @n . V.fromSized . coerce
-
-  decode _ (Constant v) = Just $ unwrapValue v
-  decode sol (Plus x y) = liftA2 (+)   (decode sol x) (decode sol y)
-  decode sol (Neg x)    = fmap negate  (decode sol x)
-  decode sol (Mul x y)  = liftA2 (*)   (decode sol x) (decode sol y)
-  decode sol (Abs x)    = fmap abs     (decode sol x)
-  decode sol (Mod x y)  = liftA2 mod   (decode sol x) (decode sol y)
-  decode sol (IDiv x y) = liftA2 div   (decode sol x) (decode sol y)
-  decode sol (Div x y)  = liftA2 (/)   (decode sol x) (decode sol y)
-  decode sol (LTH x y)  = liftA2 (<)   (decode sol x) (decode sol y)
-  decode sol (LTHE x y) = liftA2 (<=)  (decode sol x) (decode sol y)
-  decode sol (EQU x y)  = liftA2 (==)  (decode sol x) (decode sol y)
-  decode sol (Distinct x y)  = liftA2 (/=)  (decode sol x) (decode sol y)
-  decode sol (GTHE x y) = liftA2 (>=)  (decode sol x) (decode sol y)
-  decode sol (GTH x y)  = liftA2 (>)   (decode sol x) (decode sol y)
-  decode sol (Not x)    = fmap   not  (decode sol x)
-  decode sol (And x y)  = liftA2 (&&) (decode sol x) (decode sol y)
-  decode sol (Or x y)   = liftA2 (||) (decode sol x) (decode sol y)
-  decode sol (Impl x y) = liftA2 (==>) (decode sol x) (decode sol y)
-  decode sol (Xor x y)  = liftA2 xor   (decode sol x) (decode sol y)
-  decode _ Pi           = Just pi
-  decode sol (Sqrt x)   = fmap sqrt  (decode sol x)
-  decode sol (Exp x)    = fmap exp   (decode sol x)
-  decode sol (Sin x)    = fmap sin   (decode sol x)
-  decode sol (Cos x)    = fmap cos   (decode sol x)
-  decode sol (Tan x)    = fmap tan   (decode sol x)
-  decode sol (Asin x)   = fmap asin  (decode sol x)
-  decode sol (Acos x)   = fmap acos  (decode sol x)
-  decode sol (Atan x)   = fmap atan  (decode sol x)
-  decode sol (ToReal x) = fmap realToFrac (decode sol x)
-  decode sol (ToInt x)  = fmap truncate   (decode sol x)
-  decode sol (IsInt x)  = fmap ((0 ==) . snd . properFraction) (decode sol x)
-  decode sol (Ite p t f) = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) 
+  decode sol (Var var)  = do
+    (IntValueMap m) <- DMap.lookup (sortSing @t) sol
+    val <- IM.lookup (coerce var) m
+    return $ unwrapValue val
+  decode _ (Constant v)         = Just $ unwrapValue v
+  decode sol (Plus x y)         = liftA2 (+)   (decode sol x) (decode sol y)
+  decode sol (Neg x)            = fmap negate  (decode sol x)
+  decode sol (Mul x y)          = liftA2 (*)   (decode sol x) (decode sol y)
+  decode sol (Abs x)            = fmap abs     (decode sol x)
+  decode sol (Mod x y)          = liftA2 mod   (decode sol x) (decode sol y)
+  decode sol (IDiv x y)         = liftA2 div   (decode sol x) (decode sol y)
+  decode sol (Div x y)          = liftA2 (/)   (decode sol x) (decode sol y)
+  decode sol (LTH x y)          = liftA2 (<)   (decode sol x) (decode sol y)
+  decode sol (LTHE x y)         = liftA2 (<=)  (decode sol x) (decode sol y)
+  decode sol (EQU x y)          = liftA2 (==)  (decode sol x) (decode sol y)
+  decode sol (Distinct x y)     = liftA2 (/=)  (decode sol x) (decode sol y)
+  decode sol (GTHE x y)         = liftA2 (>=)  (decode sol x) (decode sol y)
+  decode sol (GTH x y)          = liftA2 (>)   (decode sol x) (decode sol y)
+  decode sol (Not x)            = fmap   not  (decode sol x)
+  decode sol (And x y)          = liftA2 (&&) (decode sol x) (decode sol y)
+  decode sol (Or x y)           = liftA2 (||) (decode sol x) (decode sol y)
+  decode sol (Impl x y)         = liftA2 (==>) (decode sol x) (decode sol y)
+  decode sol (Xor x y)          = liftA2 xor   (decode sol x) (decode sol y)
+  decode _ Pi                   = Just pi
+  decode sol (Sqrt x)           = fmap sqrt  (decode sol x)
+  decode sol (Exp x)            = fmap exp   (decode sol x)
+  decode sol (Sin x)            = fmap sin   (decode sol x)
+  decode sol (Cos x)            = fmap cos   (decode sol x)
+  decode sol (Tan x)            = fmap tan   (decode sol x)
+  decode sol (Asin x)           = fmap asin  (decode sol x)
+  decode sol (Acos x)           = fmap acos  (decode sol x)
+  decode sol (Atan x)           = fmap atan  (decode sol x)
+  decode sol (ToReal x)         = fmap realToFrac (decode sol x)
+  decode sol (ToInt x)          = fmap truncate   (decode sol x)
+  decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)
+  decode sol (Ite p t f)        = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) 
   decode sol (BvNot x)          = fmap not (decode sol x)
   decode sol (BvAnd x y)        = liftA2 (&&) (decode sol x) (decode sol y)
   decode sol (BvOr x y)         = liftA2 (||) (decode sol x) (decode sol y)
@@ -115,8 +99,11 @@
   decode sol (BvuLTHE x y)      = liftA2 (<=) (decode sol x) (decode sol y)
   decode sol (BvuGTHE x y)      = liftA2 (>=) (decode sol x) (decode sol y)
   decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
-  decode _ (ForAll _ _)       = Nothing
-  decode _ (Exists _ _)       = Nothing
+  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 _ (ForAll _ _)         = Nothing
+  decode _ (Exists _ _)         = Nothing
+  
   encode = Constant . wrapValue
 
 instance Codec () where
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
@@ -2,12 +2,16 @@
 {-# LANGUAGE NoStarIsType #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Language.Hasmtlib.Internal.Expr where
 
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Boolean
+import Data.GADT.Compare
+import Data.Map
 import Data.Kind
 import Data.Proxy
 import Data.Coerce
@@ -16,70 +20,129 @@
 import GHC.TypeLits
 
 -- | Sorts in SMTLib2 - used as promoted type (data-kind).
-data SMTSort = IntSort | RealSort | BoolSort | BvSort Nat
+data SMTSort =
+    BoolSort                      -- ^ Sort of Bool
+  | IntSort                       -- ^ Sort of Int
+  | RealSort                      -- ^ Sort of Real
+  | BvSort Nat                    -- ^ Sort of BitVec with length n
+  | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v
 
 -- | 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)
 $(makeLenses ''SMTVar)
 
--- | Injective type-family that computes the Haskell 'Type' of a 'SMTSort'.
+-- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.
 type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
-  HaskellType IntSort    = Integer
-  HaskellType RealSort   = Double
-  HaskellType BoolSort   = Bool
-  HaskellType (BvSort n) = Bitvec n
+  HaskellType IntSort         = Integer
+  HaskellType RealSort        = Double
+  HaskellType BoolSort        = Bool
+  HaskellType (BvSort n)      = Bitvec n
+  HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)
 
 -- | 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)
+  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)
 
--- | Unwrap a value.
+-- | 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
 {-# INLINEABLE unwrapValue #-}
 
--- | Wrap a value.
+-- | 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
+  SArraySort _ _ -> ArrayValue
 {-# INLINEABLE wrapValue #-}
 
-deriving instance Show (Value t)
-deriving instance Eq   (Value t)
-deriving instance Ord  (Value t)
-
 -- | 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)
+  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)
 
 deriving instance Show (SSMTSort t)
 deriving instance Eq   (SSMTSort t)
 deriving instance Ord  (SSMTSort t)
 
+instance GEq SSMTSort where
+  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
+    Just Refl -> Just Refl
+    Nothing   -> Nothing
+  geq _ _                     = Nothing
+
+instance GCompare SSMTSort where
+  gcompare SBoolSort SBoolSort     = GEQ
+  gcompare SIntSort SIntSort       = GEQ
+  gcompare SRealSort SRealSort     = GEQ
+  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of
+    LTI -> GLT
+    EQI -> GEQ
+    GTI -> GGT
+  gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of
+    GLT -> GLT
+    GEQ -> case gcompare (sortSing' v) (sortSing' v') of
+      GLT -> GLT
+      GEQ -> GEQ
+      GGT -> GGT
+    GGT -> GGT
+  gcompare SBoolSort _        = GLT
+  gcompare _ SBoolSort        = GGT
+  gcompare SIntSort _         = GLT
+  gcompare _ SIntSort         = GGT
+  gcompare SRealSort _        = GLT
+  gcompare _ SRealSort        = GGT
+  gcompare (SArraySort _ _) _ = GLT
+  gcompare _ (SArraySort _ _) = GGT
+
 -- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.
 class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t
 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 (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where
+   sortSing = SArraySort (Proxy @k) (Proxy @v)
 
--- | An existential wrapper that hides some 'SMTSort'.
-data SomeKnownSMTSort f where
-  SomeKnownSMTSort :: forall (t :: SMTSort) f. KnownSMTSort t => f t -> SomeKnownSMTSort f
+-- | Wrapper for 'sortSing' which takes a 'Proxy'
+sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
+sortSing' _ = sortSing @t
 
+-- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k
+-- 
+-- @
+-- AllC '[]       k = ()
+-- AllC (c ': cs) k = (c k, AllC cs k)
+-- @ 
+type AllC :: [k -> Constraint] -> k -> Constraint
+type family AllC cs k :: Constraint where
+  AllC '[]       k = ()
+  AllC (c ': cs) k = (c k, AllC cs k)
+
+-- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.
+data SomeSMTSort cs f where
+  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f
+
+-- | An existential wrapper that hides some known 'SMTSort'.
+type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f 
+
 -- | A SMT expression.
 --   For internal use only.
 --   For building expressions use the corresponding instances (Num, Boolean, ...).
@@ -108,47 +171,50 @@
   Impl      :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
   Xor       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
 
-  Pi       :: Expr RealSort
-  Sqrt     :: Expr RealSort -> Expr RealSort
-  Exp      :: Expr RealSort -> Expr RealSort
-  Sin      :: Expr RealSort -> Expr RealSort
-  Cos      :: Expr RealSort -> Expr RealSort
-  Tan      :: Expr RealSort -> Expr RealSort
-  Asin     :: Expr RealSort -> Expr RealSort
-  Acos     :: Expr RealSort -> Expr RealSort
-  Atan     :: Expr RealSort -> Expr RealSort
+  Pi        :: Expr RealSort
+  Sqrt      :: Expr RealSort -> Expr RealSort
+  Exp       :: Expr RealSort -> Expr RealSort
+  Sin       :: Expr RealSort -> Expr RealSort
+  Cos       :: Expr RealSort -> Expr RealSort
+  Tan       :: Expr RealSort -> Expr RealSort
+  Asin      :: Expr RealSort -> Expr RealSort
+  Acos      :: Expr RealSort -> Expr RealSort
+  Atan      :: Expr RealSort -> Expr RealSort
 
-  ToReal   :: Expr IntSort  -> Expr RealSort
-  ToInt    :: Expr RealSort -> Expr IntSort
-  IsInt    :: Expr RealSort -> Expr BoolSort
+  ToReal    :: Expr IntSort  -> Expr RealSort
+  ToInt     :: Expr RealSort -> Expr IntSort
+  IsInt     :: Expr RealSort -> Expr BoolSort
 
-  Ite      :: Expr BoolSort -> Expr t -> Expr t -> Expr t
+  Ite       :: Expr BoolSort -> Expr t -> Expr t -> Expr t
 
-  BvNot    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
-  BvAnd    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvOr     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvXor    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvNand   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvNor    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvNeg    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
-  BvAdd    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvSub    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvMul    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvuDiv   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvuRem   :: 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, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
-  BvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
-  BvuLT    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
-  BvuLTHE  :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
-  BvuGTHE  :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
-  BvuGT    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+  BvNot     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
+  BvAnd     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvOr      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvXor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvNand    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvNor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvNeg     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
+  BvAdd     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvSub     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvMul     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvuDiv    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvuRem    :: 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, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
+  BvRotR    :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
+  BvuLT     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+  BvuLTHE   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+  BvuGTHE   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+  BvuGT     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
 
-  ForAll   :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
-  Exists   :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
+  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)
 
+  ForAll    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
+  Exists    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
+
 instance Boolean (Expr BoolSort) where
   bool = Constant . BoolValue
   {-# INLINE bool #-}
@@ -182,22 +248,35 @@
   maxBound = Constant $ BvValue maxBound
 
 instance Render (SSMTSort t) where
+  render SBoolSort   = "Bool"
   render SIntSort    = "Int"
   render SRealSort   = "Real"
-  render SBoolSort   = "Bool"
   render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
+  render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)
   {-# INLINEABLE render #-}
 
 instance Render (SMTVar t) where
   render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)
   {-# INLINEABLE render #-}
 
+instance Render (Value t) where
+  render (IntValue x)   = render x
+  render (RealValue x)  = render x
+  render (BoolValue x)  = render x
+  render (BvValue   v)  = "#b" <> render v
+  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of
+    Nothing -> constRender $ arr^.arrConst
+    Just ((k,v), stored')
+      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))
+      | otherwise  -> constRender v
+    where
+      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)
+
 instance KnownSMTSort t => Render (Expr t) where
-  render (Var v)                  = render v
-  render (Constant (IntValue x))  = render x
-  render (Constant (RealValue x)) = render x
-  render (Constant (BoolValue x)) = render x
-  render (Constant (BvValue   v)) = "#b" <> render v
+  render (Var v)      = render v
+  render (Constant c) = render c
 
   render (Plus x y)   = renderBinary "+" x y
   render (Neg x)      = renderUnary  "-" x
@@ -258,6 +337,9 @@
   render (BvuGTHE x y)      = renderBinary "bvuge"  (render x) (render y)
   render (BvuGT x y)        = renderBinary "bvugt"  (render x) (render y)
 
+  render (ArrSelect a i)    = renderBinary  "select" (render a) (render i)
+  render (ArrStore a i v)   = renderTernary "store"  (render a) (render i) (render v)
+
   render (ForAll mQvar f) = renderQuantifier "forall" mQvar f
   render (Exists mQvar f) = renderQuantifier "exists" mQvar f
 
@@ -271,65 +353,71 @@
     expr = render $ f $ Var qvar
 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
+
 instance Show (Expr t) where
-  show (Var v)                  = show v
-  show (Constant (IntValue x))  = show x
-  show (Constant (RealValue x)) = show x
-  show (Constant (BoolValue x)) = show x
-  show (Constant (BvValue   x)) = show x
-  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 x y)                = "(" ++ show x ++ " == " ++ show y ++ ")"
-  show (Distinct x y)           = "(" ++ show x ++ " /= " ++ show y ++ ")"
-  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 (Exists (Just qv) f)     = "(exists " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
-  show (Exists Nothing f)       = "(exists var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
+  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 x y)            = "(" ++ show x ++ " == " ++ show y ++ ")"
+  show (Distinct x y)       = "(" ++ show x ++ " /= " ++ show y ++ ")"
+  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)))) ++ ")"
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
@@ -1,4 +1,5 @@
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE LiberalTypeSynonyms #-}
 
 module Language.Hasmtlib.Internal.Parser where
 
@@ -12,6 +13,7 @@
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Type.ArrayMap
 import Data.Bit
 import Data.Coerce
 import Data.Proxy
@@ -20,7 +22,6 @@
 import Data.ByteString.Builder
 import Data.Attoparsec.ByteString hiding (Result, skipWhile)
 import Data.Attoparsec.ByteString.Char8 hiding (Result)
-import qualified Data.IntMap as IM
 import Control.Applicative
 import Control.Lens hiding (op)
 import GHC.TypeNats
@@ -47,7 +48,7 @@
   varSols <- many $ parseSomeSol <* skipSpace
   _       <- (skipSpace >> char ')' >> skipSpace) <|> skipSpace
 
-  return $ fromSomeList varSols
+  return $ fromSomeVarSols varSols
 
 smt2ModelParser :: Parser Solution
 smt2ModelParser = do
@@ -55,46 +56,64 @@
   varSols <- many $ parseSomeSol <* skipSpace
   _       <- (skipSpace >> char ')' >> skipSpace) <|> skipSpace
 
-  return $ fromSomeList varSols
-
-fromSomeList :: [SomeKnownSMTSort SMTVarSol] -> Solution
-fromSomeList = IM.fromList . fmap (\case someVarSol@(SomeKnownSMTSort varSol) -> (coerce (varSol^.solVar), someVarSol))
-
-parseSomeSol :: Parser (SomeKnownSMTSort SMTVarSol)
-parseSomeSol = SomeKnownSMTSort <$> (parseSol @IntSort)
-           <|> SomeKnownSMTSort <$> (parseSol @RealSort)
-           <|> SomeKnownSMTSort <$> (parseSol @BoolSort)
-           <|> parseAnyBvUpToLength 128
-
-parseAnyBvUpToLength :: Natural -> Parser (SomeKnownSMTSort SMTVarSol)
-parseAnyBvUpToLength hi = asum $ fmap ((\case SomeNat p -> goProxy p) . someNatVal) [0..hi]
-  where
-    goProxy :: forall n. KnownNat n => Proxy n -> Parser (SomeKnownSMTSort SMTVarSol)
-    goProxy _ = SomeKnownSMTSort <$> parseSol @(BvSort n)
+  return $ fromSomeVarSols varSols
 
-parseSol :: forall t. KnownSMTSort t => Parser (SMTVarSol t)
-parseSol = do
+parseSomeSol :: Parser (SomeKnownOrdSMTSort SMTVarSol)
+parseSomeSol = do
   _     <- char '(' >> skipSpace
   _     <- string "define-fun" >> skipSpace
   _     <- string "var_"
   vId   <- decimal @Int
   _     <- skipSpace >> string "()" >> skipSpace
-  _     <- string $ toStrict $ toLazyByteString $ render (sortSing @t)
+  (SomeSMTSort someSort) <- parseSomeSort
   _     <- skipSpace
-  expr  <- parseExpr @t
+  expr  <- parseExpr' someSort
   _     <- skipSpace >> char ')'
-
-  -- Try to evaluate expression given by solver as solution
-  -- Better: Take into scope already successfully parsed solutions for other vars.
-  -- Is this even required though? Do the solvers ever answer like-wise?
   case decode mempty expr of
     Nothing    -> fail $ "Solver reponded with solution for var_" ++ show vId ++ " but it contains "
                       ++ "another var. This cannot be parsed and evaluated currently."
-    Just value -> return $ SMTVarSol (coerce vId) (wrapValue value)
-{-# INLINEABLE parseSol #-}
+    Just value -> return $ SomeSMTSort $ SMTVarSol (coerce vId) (wrapValue value)
+{-# INLINEABLE parseSomeSol #-}
 
+parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
+parseSomeSort = (string "Bool" *> pure (SomeSMTSort SBoolSort))
+        <|> (string "Int"  *> pure (SomeSMTSort SIntSort))
+        <|> (string "Real" *> pure (SomeSMTSort SRealSort))
+        <|> parseSomeBitVecSort
+        <|> parseSomeArraySort
+{-# INLINEABLE parseSomeSort #-}
+
+parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
+parseSomeBitVecSort = do
+  _ <- char '(' >> skipSpace >> char '_' >> skipSpace
+  _ <- string "BitVec" >> skipSpace
+  n <- decimal
+  _ <- skipSpace >> char ')'
+  case someNatVal $ fromInteger n of
+    SomeNat pn -> return $ SomeSMTSort $ SBvSort pn
+{-# INLINEABLE parseSomeBitVecSort #-}
+
+parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
+parseSomeArraySort = do
+  _ <- char '(' >> skipSpace
+  _ <- string "Array" >> skipSpace
+  (SomeSMTSort keySort)   <- parseSomeSort
+  _ <- skipSpace
+  (SomeSMTSort valueSort) <- parseSomeSort
+  _ <- skipSpace >> char ')'
+  return $ SomeSMTSort $ SArraySort (goProxy keySort) (goProxy valueSort)
+    where
+      goProxy :: forall t. SSMTSort t -> Proxy t
+      goProxy _ = Proxy @t
+{-# INLINEABLE parseSomeArraySort #-}
+
+parseExpr' :: forall prxy t. KnownSMTSort t => prxy t -> Parser (Expr t)
+parseExpr' _ = parseExpr @t
+{-# INLINE parseExpr' #-}
+
+-- TODO: Add parseSelect
 parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
-parseExpr = var <|> constant <|> smtIte
+parseExpr = var <|> constantExpr <|> smtIte
         <|> case sortSing @t of
               SIntSort  -> unary "abs" abs <|> unary  "-" negate
                       <|> nary "+" sum  <|> binary "-" (-) <|> nary "*" product <|> binary "mod" Mod
@@ -115,15 +134,15 @@
                       <|> binary @IntSort ">=" (>=?) <|> binary @IntSort ">" (>?)
                       <|> binary @RealSort "<" (<?) <|> binary @RealSort "<=" (<=?)
                       <|> binary @RealSort ">=" (>=?) <|> binary @RealSort ">" (>?)
-                      -- TODO: All (?) bv lengths - also for '=' and 'distinct'
---                      <|> binary @(BvSort 10) "bvult" (<?) <|> binary @(BvSort 10) "bvule" (<=?)
---                      <|> binary @(BvSort 10) "bvuge" (>=?) <|> binary @(BvSort 10) "bvugt" (>?)
+                      -- 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
                       <|> unary  "bvneg" negate
                       <|> binary "bvadd" (+)  <|> binary "bvsub" (-) <|> binary "bvmul" (*)
                       <|> binary "bvudiv" BvuDiv <|> binary "bvurem" BvuRem
                       <|> binary "bvshl" BvShL <|> binary "bvlshr" BvLShR
+              SArraySort _ _ -> parseStore
+                      -- TODO: Add compare ops for all (?) array-sorts
 
 var :: Parser (Expr t)
 var = do
@@ -131,21 +150,24 @@
   vId <- decimal @Int
 
   return $ Var $ coerce vId
-{-# INLINEABLE var #-}
+{-# INLINE var #-}
 
-constant :: forall t. KnownSMTSort t => Parser (Expr t)
-constant = do
-  cval <- case sortSing @t of
-    SIntSort  -> anyValue decimal
-    SRealSort -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational
-    SBoolSort -> parseBool
-    SBvSort p -> anyBitvector p
+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
+  SArraySort k v -> constArray k v
+{-# INLINE constant #-}
 
-  return $ Constant $ wrapValue cval
-{-# 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 p = binBitvector p <|> hexBitvector p <|> literalBitvector p
+{-# INLINE anyBitvector #-}
 
 binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 binBitvector p = do
@@ -161,7 +183,7 @@
 hexBitvector _ = do
   _ <- string "#x" >> skipSpace
   fromInteger <$> hexadecimal
-{-# INLINEABLE hexBitvector #-}
+{-# INLINE hexBitvector #-}
 
 literalBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 literalBitvector _ = do
@@ -172,8 +194,44 @@
   _ <- skipWhile (/= ')') >> char ')'
 
   return $ fromInteger x
-{-# INLINEABLE literalBitvector #-}
+{-# INLINE literalBitvector #-}
 
+constArray :: forall k v. (KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))
+constArray _ _ = do
+  _ <- char '(' >> skipSpace >> char '(' >> skipSpace
+  _ <- string "as" >> skipSpace >> string "const" >> skipSpace
+  _ <- char '(' >> skipWhile (/= ')') >> char ')' >> skipSpace
+  _ <- char ')' >> skipSpace
+  constVal <- constant @v
+  _ <- skipSpace >> char ')'
+
+  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
+
 unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
 unary opStr op = do
   _ <- char '(' >> skipSpace
@@ -182,7 +240,7 @@
   _ <- skipSpace >> char ')'
 
   return $ op val
-{-# INLINEABLE unary #-}
+{-# INLINE unary #-}
 
 binary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
 binary opStr op = do
@@ -193,7 +251,7 @@
   r <- parseExpr
   _ <- skipSpace >> char ')'
   return $ l `op` r
-{-# INLINEABLE binary #-}
+{-# INLINE binary #-}
 
 nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
 nary opStr op = do
@@ -202,11 +260,11 @@
   args <- parseExpr `sepBy1` skipSpace
   _    <- skipSpace >> char ')'
   return $ op args
-{-# INLINEABLE nary #-}
+{-# INLINE nary #-}
 
 smtPi :: Parser (Expr RealSort)
 smtPi = string "real.pi" *> return pi
-{-# INLINEABLE smtPi #-}
+{-# INLINE smtPi #-}
 
 toRealFun :: Parser (Expr RealSort)
 toRealFun = do
@@ -263,7 +321,7 @@
   _ <- skipSpace >> char ')'
 
   return $ negate val
-{-# INLINEABLE negativeValue #-}
+{-# INLINE negativeValue #-}
 
 parseRatioDouble :: Parser Double
 parseRatioDouble = do
diff --git a/src/Language/Hasmtlib/Solver/CVC5.hs b/src/Language/Hasmtlib/Solver/CVC5.hs
--- a/src/Language/Hasmtlib/Solver/CVC5.hs
+++ b/src/Language/Hasmtlib/Solver/CVC5.hs
@@ -3,7 +3,5 @@
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
--- TODO: Add support for lib binding: https://github.com/tweag/smtlib-backends/tree/master/smtlib-backends-cvc5
-
 cvc5 :: ProcessSolver
 cvc5 = ProcessSolver $ P.defaultConfig { P.exe = "cvc5", P.args = [] }
diff --git a/src/Language/Hasmtlib/Solver/Z3.hs b/src/Language/Hasmtlib/Solver/Z3.hs
--- a/src/Language/Hasmtlib/Solver/Z3.hs
+++ b/src/Language/Hasmtlib/Solver/Z3.hs
@@ -3,8 +3,6 @@
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
--- TODO: Add support for lib binding: https://github.com/tweag/smtlib-backends/tree/master/smtlib-backends-z3
-
 z3 :: ProcessSolver
 z3 = ProcessSolver P.defaultConfig
 
diff --git a/src/Language/Hasmtlib/Type/ArrayMap.hs b/src/Language/Hasmtlib/Type/ArrayMap.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Type/ArrayMap.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Language.Hasmtlib.Type.ArrayMap where
+
+import Data.Proxy
+import qualified Data.Map as Map  
+import Control.Lens
+
+-- | Class that allows access to a map-like array where specific values are is the default value or overwritten values.
+--   Every index has a value by default.
+--   Values at indices can be overwritten manually.
+-- 
+--   Based on McCarthy`s basic array theory.
+-- 
+--   Therefore the following axioms must hold:
+-- 
+-- 1. forall A i x: arrSelect (store A i x) == x
+-- 
+-- 2. forall A i j x: i /= j ==> (arrSelect (arrStore A i x) j === arrSelect A j)
+class ArrayMap f k v where
+  asConst'   :: Proxy f -> Proxy k -> v -> f k v 
+  viewConst  :: f k v -> v
+  arrSelect  :: f k v -> k -> v
+  arrStore   :: f k v -> k -> v -> f k v
+
+-- | Wrapper for 'asConst'' which hides the 'Proxy'
+asConst :: forall f k v. ArrayMap f k v => v -> f k v
+asConst = asConst' (Proxy @f) (Proxy @k)
+
+-- | A map-like array with a default constant value and partially overwritten values.  
+data ConstArray k v = ConstArray 
+  { _arrConst :: v
+  , _stored :: Map.Map k v
+  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
+$(makeLenses ''ConstArray)
+
+instance Ord k => ArrayMap ConstArray k v where
+  asConst' _ _ x = ConstArray x Map.empty
+  viewConst arr = arr^.arrConst
+  arrSelect arr i = case Map.lookup i (arr^.stored) of
+    Nothing -> viewConst arr
+    Just x  -> x
+  arrStore arr i x = arr & stored %~ Map.insert i x
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
@@ -2,12 +2,13 @@
 
 module Language.Hasmtlib.Type.Expr
  ( SMTSort(..)
- , SMTVar(..)
+ , SMTVar(..), varId
  , HaskellType
  , Value(..), unwrapValue, wrapValue
- , SSMTSort(..), KnownSMTSort(..), SomeKnownSMTSort(..)
+ , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort
  , Expr
  , for_all , exists
+ , select, store
  , module Language.Hasmtlib.Internal.Expr.Num
  )
 where
@@ -49,3 +50,11 @@
 --   It will only be scoped for the lambdas body.
 exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
 exists = Exists Nothing
+
+-- | Select a value from an array.
+select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
+select = ArrSelect
+
+-- | Store a value in an array.
+store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
+store = ArrStore
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -12,7 +12,8 @@
 import Language.Hasmtlib.Internal.Parser hiding (var, constant)
 import qualified SMTLIB.Backends as B
 import Data.List (isPrefixOf)
-import Data.IntMap (singleton)
+import Data.IntMap as IMap (singleton)
+import Data.Dependent.Map as DMap
 import Data.Coerce
 import Data.ByteString.Builder
 import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf)
@@ -97,7 +98,13 @@
       Left e    -> liftIO $ do
         print model
         error e
-      Right sol -> return $ decode (singleton (sol^.solVar.varId) (SomeKnownSMTSort sol)) v
+      Right sol -> 
+        return $ 
+          decode 
+            (DMap.singleton 
+              (sortSing @t) 
+              (IntValueMap $ IMap.singleton (sol^.solVar.varId) (sol^.solVal))) 
+            v
   getValue expr = do
     model <- getModel
     return $ decode model expr
diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs
--- a/src/Language/Hasmtlib/Type/SMT.hs
+++ b/src/Language/Hasmtlib/Type/SMT.hs
@@ -35,7 +35,7 @@
 
   var' p = do
     newVar <- smtvar' p
-    vars %= (|> SomeKnownSMTSort newVar)
+    vars %= (|> SomeSMTSort newVar)
     return $ Var newVar
   {-# INLINEABLE var' #-}
 
@@ -75,5 +75,5 @@
 {-# INLINEABLE renderAssert #-}
 
 renderVars :: Seq (SomeKnownSMTSort SMTVar) -> Seq Builder
-renderVars = fmap (\(SomeKnownSMTSort v) -> renderDeclareVar v)
+renderVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v)
 {-# INLINEABLE renderVars #-}
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -1,9 +1,14 @@
+{-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Language.Hasmtlib.Type.Solution where
 
 import Language.Hasmtlib.Type.Expr
-import Data.IntMap
+import Data.IntMap as IMap hiding (foldl)
+import Data.Dependent.Map as DMap
+import Data.Dependent.Map.Lens
 import Control.Lens
 
 -- | Function that turns a state into a result and a solution.
@@ -12,12 +17,36 @@
 -- | Results of check-sat commands.
 data Result = Unsat | Unknown | Sat deriving (Show, Eq, Ord)
 
--- | A Solution is a Map from the variable-identifier to some solution for it.
-type Solution = IntMap (SomeKnownSMTSort SMTVarSol)
+-- | A Solution is a dependent map 'DMap' from 'SSMTSort's t to 'IntMap' t.
+type Solution = DMap SSMTSort IntValueMap
 
+-- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'.
+newtype IntValueMap t = IntValueMap (IntMap (Value t))
+  deriving stock Show
+  deriving newtype (Semigroup, Monoid)
+
 -- | A solution for a single variable.
-data SMTVarSol (t :: SMTSort) = SMTVarSol 
+data SMTVarSol (t :: SMTSort) = SMTVarSol
   { _solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem
   , _solVal :: Value t                        -- ^ An assignment for this variable in a solution
-  } deriving (Show, Eq, Ord)
+  } deriving Show
 $(makeLenses ''SMTVarSol)
+
+-- | Alias class for constraint 'Ord' ('HaskellType' t)
+class Ord (HaskellType t) => OrdHaskellType t
+instance Ord (HaskellType t) => OrdHaskellType t
+
+-- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType' 
+type SomeKnownOrdSMTSort f = SomeSMTSort '[KnownSMTSort, OrdHaskellType] f
+
+-- | Create a 'Solution' from some 'SMTVarSol's.
+fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
+fromSomeVarSols = foldl
+  (\dsol (SomeSMTSort s) -> let sSort = sortSing' s in
+    dsol & dmat sSort %~
+      (\case
+        Nothing -> Just $ IntValueMap $ IMap.singleton (s^.solVar.varId) (s^.solVal)
+        Just (IntValueMap im) -> Just $ IntValueMap $ IMap.insert (s^.solVar.varId) (s^.solVal) im
+      )
+  )
+  mempty