diff --git a/boolector.cabal b/boolector.cabal
--- a/boolector.cabal
+++ b/boolector.cabal
@@ -1,5 +1,5 @@
 name:                boolector
-version:             0.0.0.3
+version:             0.0.0.4
 synopsis:            Haskell bindings for the Boolector SMT solver
 description:
 
@@ -79,11 +79,29 @@
   extra-libraries:  boolector
   hs-source-dirs: test
 
+Test-Suite Arith_Example2
+  default-language: Haskell2010
+  Build-Depends: base >= 4.7 && < 5
+               , boolector
+  Type: exitcode-stdio-1.0
+  main-is: Arith_Example2.hs
+  extra-libraries:  boolector
+  hs-source-dirs: test
+
 Test-Suite GetSetSymbol_Example
   default-language: Haskell2010
   Build-Depends: base >= 4.7 && < 5
                , boolector
   Type: exitcode-stdio-1.0
   main-is: GetSetSymbol_Example.hs
+  extra-libraries:  boolector
+  hs-source-dirs: test
+
+Test-Suite UF_Example2
+  default-language: Haskell2010
+  Build-Depends: base >= 4.7 && < 5
+               , boolector
+  Type: exitcode-stdio-1.0
+  main-is: UF_Example2.hs
   extra-libraries:  boolector
   hs-source-dirs: test
diff --git a/src/Boolector.hs b/src/Boolector.hs
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 {-|
 
 This module exposes a DSL for writing symbolic computations atop the Boolector
@@ -154,22 +155,23 @@
                  , ror
                  -- *** Arithmetic operations
                  , add
-                 , uaddo
-                 , saddo
                  , inc
                  , sub
-                 , usubo
-                 , ssubo
                  , dec
                  , mul
-                 , umulo
-                 , smulo
                  , udiv
                  , sdiv
-                 , sdivo
                  , urem
                  , srem
                  , smod
+                 -- **** Overflow detection
+                 , uaddo
+                 , saddo
+                 , usubo
+                 , ssubo
+                 , umulo
+                 , smulo
+                 , sdivo
                  -- *** Comparison operations
                  , ult
                  , slt
@@ -208,6 +210,7 @@
                  , boolAssignment
                  -- ** Sorts
                  , Sort
+                 , SortTy, sortTy
                  , boolSort
                  , bitvecSort
                  , funSort
@@ -226,16 +229,18 @@
                  , DumpFormat(..)
                  ) where
 
-import Boolector.Foreign (Option(..), Status(..), Node, Sort)
+import Boolector.Foreign (Option(..), Status(..))
 import qualified Boolector.Foreign as B
 
 import Data.Char (isDigit)
+import Data.Maybe (listToMaybe)
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.Word
 
+import Control.Applicative ((<$>))
 import Control.Monad.State.Strict
 import Control.Exception hiding (assert)
 import Control.Concurrent
@@ -313,15 +318,15 @@
 
 -- | Add a constraint.
 assert :: MonadBoolector m => Node -> m ()
-assert = liftBoolector1 B.assert
+assert = liftBoolector1 B.assert . _node
 
 -- | Add an assumption.
 assume :: MonadBoolector m => Node -> m ()
-assume = liftBoolector1 B.assume
+assume = liftBoolector1 B.assume . _node
 
 -- | Determine if assumption node is a failed assumption.
 failed :: MonadBoolector m => Node -> m Bool
-failed = liftBoolector1 B.failed
+failed = liftBoolector1 B.failed . _node
 
 -- | Add all assumptions as assertions.
 fixateAssumptions :: MonadBoolector m => m ()
@@ -360,6 +365,13 @@
 -- Expressions
 --
 
+-- | Node data type wrapping the underlying Boolector node with a show string.
+data Node = Node { _node     :: B.Node
+                 , _showNode :: String } deriving (Eq, Ord)
+
+instance Show Node where
+  show = _showNode
+
 -- | Like true and false
 bool :: MonadBoolector m => Bool -> m Node
 bool True  = true
@@ -368,35 +380,40 @@
 -- | Create constant true. This is represented by the bit vector constant one
 -- with bit width one.
 true :: MonadBoolector m => m Node
-true = liftBoolector0 B.true
+true = mkNode "true" $ liftBoolector0 B.true
 
 -- | Create bit vector constant zero with bit width one.
 false :: MonadBoolector m => m Node
-false = liftBoolector0 B.false
+false = mkNode "false" $ liftBoolector0 B.false
 
 -- | Create bit vector constant representing the bit vector @bits@.
 const :: MonadBoolector m => String -> m Node
-const = liftBoolector1 B.const
+const str = mkNode ("0b" ++ str) $ liftBoolector1 B.const str
 
 -- | Create bit vector constant representing the decimal number @str@.
 constd :: MonadBoolector m => Sort -> String -> m Node
-constd = liftBoolector2 B.constd
+constd srt str = mkNode str $ liftBoolector2 B.constd (_sort srt) str
 
 -- | Create bit vector constant representing the hexadecimal number @str@.
 consth :: MonadBoolector m => Sort -> String -> m Node
-consth = liftBoolector2 B.consth
+consth srt str = mkNode ("0x" ++ str) $ liftBoolector2 B.consth (_sort srt) str
 
 -- | Create bit vector constant zero of sort @sort@.
 zero :: MonadBoolector m => Sort -> m Node
-zero = liftBoolector1 B.zero
+zero = mkNode "zero" . liftBoolector1 B.zero . _sort
 
 -- | Create bit vector constant of sort @sort@, where each bit is set to one.
 ones :: MonadBoolector m => Sort -> m Node
-ones = liftBoolector1 B.ones
+ones srt = mkNode onesStr $ liftBoolector1 B.one $ _sort srt
+  where onesStr = "0b" ++ replicate nr '1'
+        nr = case sortTy srt of
+              BoolSort -> 1
+              BitVecSort wNr -> fromIntegral wNr
+              _ -> error "invalid sort"
 
 -- | Create bit vector constant one of sort @sort@.
 one :: MonadBoolector m => Sort -> m Node
-one = liftBoolector1 B.one
+one = mkNode "1" . liftBoolector1 B.one . _sort
 
 -- |  Create bit vector constant representing the unsigned integer @u@ of
 -- sort @sort@.
@@ -404,7 +421,7 @@
 -- The constant is obtained by either truncating bits or by unsigned extension
 -- (padding with zeroes).
 unsignedInt :: MonadBoolector m => Integer -> Sort -> m Node
-unsignedInt i sort = liftBoolector2 B.unsignedInt (fromIntegral i) sort
+unsignedInt i srt = constd srt (show i)
 
 -- | Create bit vector constant representing the signed integer @i@ of sort
 -- @sort@.
@@ -412,37 +429,38 @@
 -- The constant is obtained by either truncating bits or by
 -- signed extension (padding with ones).
 signedInt :: MonadBoolector m => Integer -> Sort -> m Node
-signedInt i sort = liftBoolector2 B.int (fromIntegral i) sort
+signedInt i srt = constd srt (show i)
 
+
 -- | Create a bit vector variable of sort @sort@.
 var :: MonadBoolector m => Sort -> String -> m Node
-var = createNamedNode B.var
+var srt str = mkNamedNode "var" B.var srt str
 
 -- | Create the one's complement of bit vector @node@.
 not :: MonadBoolector m => Node -> m Node
-not = liftBoolector1 B.not
+not n1 = mkNode ["not", show n1] $ liftBoolector1 B.not (_node n1)
 
 -- | Create the two's complement of bit vector @node@.
 neg :: MonadBoolector m => Node -> m Node
-neg = liftBoolector1 B.neg
+neg n1 = mkNode ["neg", show n1] $ liftBoolector1 B.neg (_node n1)
 
 -- | Create *or* reduction of node @node@.
 --
 -- All bits of node @node@ are combined by a Boolean *or*.
 redor :: MonadBoolector m => Node -> m Node
-redor = liftBoolector1 B.redor
+redor n1 = mkNode ["redor", show n1] $ liftBoolector1 B.redor (_node n1)
 
 -- | Create *xor* reduction of node @node@.
 --
 -- All bits of @node@ are combined by a Boolean *xor*.
 redxor :: MonadBoolector m => Node -> m Node
-redxor = liftBoolector1 B.redxor
+redxor n1 = mkNode ["redxor", show n1] $ liftBoolector1 B.redxor (_node n1)
 
 -- | Create *and* reduction of node @node@.
 --
 -- All bits of @node@ are combined by a Boolean *and*.
 redand :: MonadBoolector m => Node -> m Node
-redand = liftBoolector1 B.redand
+redand n = mkNode ["redand", show n] $ liftBoolector1 B.redand (_node n)
 
 -- | Create a bit vector slice of @node@ from index @upper@ to index @lower@.
 slice :: MonadBoolector m
@@ -450,50 +468,59 @@
       -> Word32 -- ^ Upper index which must be greater than or equal to zero, and less than the bit width of @node@.
       -> Word32 -- ^ Lower index which must be greater than or equal to zero, and less than or equal to @upper@.
       -> m Node
-slice n u l = (liftBoolector3 B.slice) n (fromIntegral u) (fromIntegral l)
+slice n u l = mkNode ["slice", show n, show u, show l] $
+              liftBoolector3 B.slice (_node n) (fromIntegral u) (fromIntegral l)
 
 -- | Create unsigned extension.
 --
 -- The bit vector @node@ is padded with @width@ * zeroes.
 uext :: MonadBoolector m => Node -> Word32 -> m Node
-uext n w = (liftBoolector2 B.uext) n $ fromIntegral w
+uext n w = mkNode ["uext", show n, show w] $
+           liftBoolector2 B.uext (_node n) (fromIntegral w)
 
 -- | Create signed extension.
 --
 -- The bit vector @node@ is padded with @width@ bits where the value
 -- depends on the value of the most significant bit of node @n@.
 sext :: MonadBoolector m => Node -> Word32 -> m Node
-sext n w = liftBoolector2 B.sext n (fromIntegral w)
+sext n w = mkNode ["sext", show n, show w] $
+           liftBoolector2 B.sext (_node n) (fromIntegral w)
 
 -- | Create the concatenation of two bit vectors.
 concat :: MonadBoolector m => Node -> Node -> m Node
-concat = liftBoolector2 B.concat
+concat n1 n2 = mkNode ["concat", show n1, show n2] $
+               liftBoolector2 B.concat (_node n1) (_node n2)
 
 -- | Create @n@ concatenations of a given node @node@.
 repeat :: MonadBoolector m => Node -> Word32 -> m Node
-repeat n w = liftBoolector2 B.repeat n (fromIntegral w)
+repeat n w = mkNode ["repeat", show n, show w] $
+             liftBoolector2 B.repeat (_node n) (fromIntegral w)
 
 -- | Create boolean implication.
 implies :: MonadBoolector m => Node -> Node -> m Node
-implies = liftBoolector2 B.implies
+implies n1 n2 = mkNode ["implies", show n1, show n2] $
+                liftBoolector2 B.implies (_node n1) (_node n2)
 
 -- | Create Boolean equivalence.
 iff :: MonadBoolector m => Node -> Node -> m Node
-iff = liftBoolector2 B.iff
+iff n1 n2 = mkNode ["iff", show n1, show n2] $
+            liftBoolector2 B.iff (_node n1) (_node n2)
 
 -- | Create bit vector or array equality.
 --
 -- Both operands are either bit vectors with the same bit width or arrays
 -- of the same type.
 eq :: MonadBoolector m => Node -> Node -> m Node
-eq = liftBoolector2 B.eq
+eq n1 n2 = mkNode ["eq", show n1, show n2] $
+           liftBoolector2 B.eq (_node n1) (_node n2)
 
 -- | Create bit vector or array inequality.
 --
 -- Both operands are either bit vectors with the same bit width or arrays
 -- of the same type.
 ne :: MonadBoolector m => Node -> Node -> m Node
-ne = liftBoolector2 B.ne
+ne n1 n2 = mkNode ["ne", show n1, show n2] $
+           liftBoolector2 B.ne (_node n1) (_node n2)
 
 -- | Create an if-then-else.
 --
@@ -505,7 +532,8 @@
      -> Node -- ^ Then node
      -> Node -- ^ Else node
      -> m Node
-cond = liftBoolector3 B.cond
+cond n1 n2 n3 = mkNode ["cond", show n1, show n2, show n3] $
+                liftBoolector3 B.cond (_node n1) (_node n2) (_node n3)
 
 --
 -- Bit-wise operations.
@@ -513,27 +541,27 @@
 
 -- | Create a bit vector *xor*.
 xor :: MonadBoolector m => Node -> Node -> m Node
-xor = liftBoolector2 B.xor
+xor n1 n2 = mkNode ["xor", show n1, show n2] $ liftBoolector2 B.xor (_node n1) (_node n2)
 
 -- | Create a bit vector *xnor*.
 xnor :: MonadBoolector m => Node -> Node -> m Node
-xnor = liftBoolector2 B.xnor
+xnor n1 n2 = mkNode ["xnor", show n1, show n2] $ liftBoolector2 B.xnor (_node n1) (_node n2)
 
 -- | Create a bit vector *and*.
 and  :: MonadBoolector m => Node -> Node -> m Node
-and  = liftBoolector2 B.and
+and n1 n2 = mkNode ["and", show n1, show n2] $ liftBoolector2 B.and (_node n1) (_node n2)
 
 -- | Create a bit vector *nand*.
 nand :: MonadBoolector m => Node -> Node -> m Node
-nand = liftBoolector2 B.nand
+nand n1 n2 = mkNode ["nand", show n1, show n2] $ liftBoolector2 B.nand (_node n1) (_node n2)
 
 -- | Create a bit vector *or*.
 or :: MonadBoolector m => Node -> Node -> m Node
-or = liftBoolector2 B.or
+or n1 n2 = mkNode ["or", show n1, show n2] $ liftBoolector2 B.or (_node n1) (_node n2)
 
 -- | Create a bit vector *nor*.
 nor :: MonadBoolector m => Node -> Node -> m Node
-nor = liftBoolector2 B.nor
+nor n1 n2 = mkNode ["nor", show n1, show n2] $ liftBoolector2 B.nor (_node n1) (_node n2)
 
 -- | Create a logical shift left.
 --
@@ -543,7 +571,7 @@
     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.
     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.
     -> m Node
-sll = liftBoolector2 B.sll
+sll n1 n2 = mkNode ["sll", show n1, show n2] $ liftBoolector2 B.sll (_node n1) (_node n2)
 
 -- | Create a logical shift right.
 --
@@ -553,7 +581,7 @@
     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.
     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.
     -> m Node
-srl = liftBoolector2 B.srl
+srl n1 n2 = mkNode ["srl", show n1, show n2] $ liftBoolector2 B.srl (_node n1) (_node n2)
 
 -- | Create an arithmetic shift right.
 --
@@ -563,7 +591,7 @@
     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.
     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.
     -> m Node
-sra = liftBoolector2 B.sra
+sra n1 n2 = mkNode ["sra", show n1, show n2] $ liftBoolector2 B.sra (_node n1) (_node n2)
 
 -- | Create a rotate left.
 --
@@ -573,7 +601,7 @@
     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.
     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.
     -> m Node
-rol = liftBoolector2 B.rol
+rol n1 n2 = mkNode ["rol", show n1, show n2] $ liftBoolector2 B.rol (_node n1) (_node n2)
 
 -- | Create a rotate right.
 --
@@ -583,7 +611,7 @@
     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.
     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.
     -> m Node
-ror = liftBoolector2 B.ror
+ror n1 n2 = mkNode ["ror", show n1, show n2] $ liftBoolector2 B.ror (_node n1) (_node n2)
 
 --
 -- Arithmetic operations.
@@ -591,107 +619,125 @@
 
 -- | Create bit vector addition.
 add :: MonadBoolector m => Node -> Node -> m Node
-add = liftBoolector2 B.add
-
--- | Create an unsigned bit vector addition overflow detection.
-uaddo :: MonadBoolector m => Node -> Node -> m Node
-uaddo = liftBoolector2 B.uaddo
-
--- | Create a signed bit vector addition overflow detection.
-saddo :: MonadBoolector m => Node -> Node -> m Node
-saddo = liftBoolector2 B.saddo
+add n1 n2 = mkNode ["add", show n1, show n2] $ liftBoolector2 B.add (_node n1) (_node n2)
 
 -- | Create bit vector expression that increments bit vector @node@ by one.
 inc :: Node ->  Boolector Node
-inc = liftBoolector1 B.inc
+inc n = mkNode ["inc", show n] $ liftBoolector1 B.inc (_node n)
 
 -- | Create a bit vector subtraction.
 sub :: MonadBoolector m => Node -> Node -> m Node
-sub = liftBoolector2 B.sub
-
--- | Create an unsigned bit vector subtraction overflow detection.
-usubo :: MonadBoolector m => Node -> Node -> m Node
-usubo = liftBoolector2 B.usubo
-
--- | Create a signed bit vector subtraction overflow detection.
-ssubo :: MonadBoolector m => Node -> Node -> m Node
-ssubo = liftBoolector2 B.ssubo
+sub n1 n2 = mkNode ["sub", show n1, show n2] $ liftBoolector2 B.sub (_node n1) (_node n2)
 
 -- | Create bit vector expression that decrements bit vector @node@ by one.
 dec :: MonadBoolector m => Node -> m Node
-dec = liftBoolector1 B.dec
+dec n = mkNode ["dec", show n] $ liftBoolector1 B.dec (_node n)
 
 -- | Create a bitvector multiplication.
 mul :: MonadBoolector m => Node -> Node -> m Node
-mul = liftBoolector2 B.mul
-
--- | Create an unsigned bit vector multiplication overflow detection.
-umulo :: MonadBoolector m => Node -> Node -> m Node
-umulo = liftBoolector2 B.umulo
-
--- | Create signed multiplication overflow detection.
-smulo :: MonadBoolector m => Node -> Node -> m Node
-smulo = liftBoolector2 B.smulo
+mul n1 n2 = mkNode ["mul", show n1, show n2] $ liftBoolector2 B.mul (_node n1) (_node n2)
 
 -- | Create unsigned division.
 udiv :: MonadBoolector m => Node -> Node -> m Node
-udiv = liftBoolector2 B.udiv
+udiv n1 n2 = mkNode ["udiv", show n1, show n2] $ liftBoolector2 B.udiv (_node n1) (_node n2)
 
 -- | Create signed division.
 sdiv :: MonadBoolector m => Node -> Node -> m Node
-sdiv = liftBoolector2 B.sdiv
-
--- | Create a signed bit vector division overflow detection.
-sdivo :: MonadBoolector m => Node -> Node -> m Node
-sdivo = liftBoolector2 B.sdivo
+sdiv n1 n2 = mkNode ["sdiv", show n1, show n2] $ liftBoolector2 B.sdiv (_node n1) (_node n2)
 
 -- | Create an unsigned remainder.
 urem :: MonadBoolector m => Node -> Node -> m Node
-urem = liftBoolector2 B.urem
+urem n1 n2 = mkNode ["urem", show n1, show n2] $ liftBoolector2 B.urem (_node n1) (_node n2)
 
 -- | Create a signed remainder.
 srem :: MonadBoolector m => Node -> Node -> m Node
-srem = liftBoolector2 B.srem
+srem n1 n2 = mkNode ["srem", show n1, show n2] $ liftBoolector2 B.srem (_node n1) (_node n2)
 
 -- | Create a, signed remainder where its sign matches the sign of the divisor.
 smod :: MonadBoolector m => Node -> Node -> m Node
-smod = liftBoolector2 B.smod
+smod n1 n2 = mkNode ["smod", show n1, show n2] $ liftBoolector2 B.smod (_node n1) (_node n2)
 
 --
+-- Overflow detection
+--
+
+-- | Create an unsigned bit vector subtraction overflow detection.
+-- Returns bit vector with bit-width one, which indicates if the operation
+-- overflows.
+usubo :: MonadBoolector m => Node -> Node -> m Node
+usubo n1 n2 = mkNode ["usubo", show n1, show n2] $ liftBoolector2 B.usubo (_node n1) (_node n2)
+
+-- | Create a signed bit vector subtraction overflow detection.
+-- Returns bit vector with bit-width one, which indicates if the operation
+-- overflows.
+ssubo :: MonadBoolector m => Node -> Node -> m Node
+ssubo n1 n2 = mkNode ["ssubo", show n1, show n2] $ liftBoolector2 B.ssubo (_node n1) (_node n2)
+
+-- | Create an unsigned bit vector addition overflow detection.
+-- Returns bit vector with bit-width one, which indicates if the operation
+-- overflows.
+uaddo :: MonadBoolector m => Node -> Node -> m Node
+uaddo n1 n2 = mkNode ["uaddo", show n1, show n2] $ liftBoolector2 B.uaddo (_node n1) (_node n2)
+
+-- | Create a signed bit vector addition overflow detection.
+-- Returns bit vector with bit-width one, which indicates if the operation
+-- overflows.
+saddo :: MonadBoolector m => Node -> Node -> m Node
+saddo n1 n2 = mkNode ["saddo", show n1, show n2] $ liftBoolector2 B.saddo (_node n1) (_node n2)
+
+-- | Create an unsigned bit vector multiplication overflow detection.
+-- Returns bit vector with bit-width one, which indicates if the operation
+-- overflows.
+umulo :: MonadBoolector m => Node -> Node -> m Node
+umulo n1 n2 = mkNode ["umulo", show n1, show n2] $ liftBoolector2 B.umulo (_node n1) (_node n2)
+
+-- | Create signed multiplication overflow detection.
+-- Returns bit vector with bit-width one, which indicates if the operation
+-- overflows.
+smulo :: MonadBoolector m => Node -> Node -> m Node
+smulo n1 n2 = mkNode ["smulo", show n1, show n2] $ liftBoolector2 B.smulo (_node n1) (_node n2)
+
+-- | Create a signed bit vector division overflow detection.
+-- Returns bit vector with bit-width one, which indicates if the operation
+-- overflows.
+sdivo :: MonadBoolector m => Node -> Node -> m Node
+sdivo n1 n2 = mkNode ["sdivo", show n1, show n2] $ liftBoolector2 B.sdivo (_node n1) (_node n2)
+
+--
 -- Comparison operations.
 --
 
 -- | Create an unsigned less than.
 ult :: MonadBoolector m => Node -> Node -> m Node
-ult = liftBoolector2 B.ult
+ult n1 n2 = mkNode ["ult", show n1, show n2] $ liftBoolector2 B.ult (_node n1) (_node n2)
 
 -- | Create a signed less than.
 slt :: MonadBoolector m => Node -> Node -> m Node
-slt = liftBoolector2 B.slt
+slt n1 n2 = mkNode ["slt", show n1, show n2] $ liftBoolector2 B.slt (_node n1) (_node n2)
 
 -- | Create an unsigned less than or equal.
 ulte :: MonadBoolector m => Node -> Node -> m Node
-ulte = liftBoolector2 B.ulte
+ulte n1 n2 = mkNode ["ulte", show n1, show n2] $ liftBoolector2 B.ulte (_node n1) (_node n2)
 
 -- | Create a signed less than or equal.
 slte :: MonadBoolector m => Node -> Node -> m Node
-slte = liftBoolector2 B.slte
+slte n1 n2 = mkNode ["slte", show n1, show n2] $ liftBoolector2 B.slte (_node n1) (_node n2)
 
 -- | Create an unsigned greater than.
 ugt :: MonadBoolector m => Node -> Node -> m Node
-ugt = liftBoolector2 B.ugt
+ugt n1 n2 = mkNode ["ugt", show n1, show n2] $ liftBoolector2 B.ugt (_node n1) (_node n2)
 
 -- | Create a signed greater than.
 sgt :: MonadBoolector m => Node -> Node -> m Node
-sgt = liftBoolector2 B.sgt
+sgt n1 n2 = mkNode ["sgt", show n1, show n2] $ liftBoolector2 B.sgt (_node n1) (_node n2)
 
 -- | Create an unsigned greater than or equal.
 ugte :: MonadBoolector m => Node -> Node -> m Node
-ugte = liftBoolector2 B.ugte
+ugte n1 n2 = mkNode ["ugte", show n1, show n2] $ liftBoolector2 B.ugte (_node n1) (_node n2)
 
 -- | Create a signed greater than or equal.
 sgte :: MonadBoolector m => Node -> Node -> m Node
-sgte = liftBoolector2 B.sgte
+sgte n1 n2 = mkNode ["sgte", show n1, show n2] $ liftBoolector2 B.sgte (_node n1) (_node n2)
 
 --
 -- Array operations
@@ -701,14 +747,14 @@
 --
 -- The name must be unique.
 array :: MonadBoolector m => Sort -> String -> m Node
-array = createNamedNode B.array
+array srt str = mkNamedNode "array" B.array srt str
 
 -- | Create a read on array @n_array@ at position @n_index@.
 read :: MonadBoolector m
      => Node -- ^ Array operand.
      -> Node -- ^ Bit vector index. The bit width of @n_index@ must have the same bit width as the indices of @n_array@.
      -> m Node
-read = liftBoolector2 B.read
+read n1 n2 = mkNode ["read", show n1, show n2] $ liftBoolector2 B.read (_node n1) (_node n2)
 
 -- | Create a write on array @n_array@ at position @n_index@ with value
 -- @n_value@.
@@ -722,7 +768,7 @@
       -> Node -- ^ Bit vector index.
       -> Node -- ^ Bit vector value.
       -> m Node
-write = liftBoolector3 B.write
+write n1 n2 n3 = mkNode ["write", show n1, show n2, show n3] $ liftBoolector3 B.write (_node n1) (_node n2) (_node n3)
 
 --
 -- Functions
@@ -732,7 +778,7 @@
 --
 -- The name must be unique.
 uf :: MonadBoolector m => Sort -> String -> m Node
-uf = createNamedNode B.uf
+uf srt str = mkNamedNode "uf" B.uf srt str
 
 -- | Create function parameter of sort @sort@.
 --
@@ -740,7 +786,7 @@
 -- used to create functions. Once a parameter is bound to a function, it
 -- cannot be re-used in other functions.
 param :: MonadBoolector m => Sort -> String -> m Node
-param = liftBoolector2 B.param
+param srt str = mkNode ["param", show srt, str] $ liftBoolector2 B.param (_sort srt) str
 
 -- | Create a function with body @node@ parameterized over parameters
 -- @param_nodes@.
@@ -753,7 +799,7 @@
     => [Node] -- ^ Parameters of function.
     -> Node   -- ^ Function body parameterized over @param_nodes@.
     -> m Node
-fun = liftBoolector2 B.fun
+fun n1 n2 = mkNode ["fun", show n1, show n2] $ liftBoolector2 B.fun (map _node n1) (_node n2)
 
 -- | Create a function application on function @n_fun@ with arguments
 -- @arg_nodes@.
@@ -761,7 +807,7 @@
       => [Node] -- ^ Arguments to be applied.
       -> Node   -- ^ Number of arguments to be applied.
       -> m Node
-apply = liftBoolector2 B.apply
+apply n1 n2 = mkNode ["apply", show n1, show n2] $  liftBoolector2 B.apply (map _node n1) (_node n2)
 
 
 --
@@ -770,17 +816,17 @@
 
 -- | Create a universally quantified term.
 forall :: MonadBoolector m
-       => [Node] -- ^ Quantified variables
-       -> Node   -- ^ Term where variables may occur
+       => [Node] -- ^ Quantified variables (create with 'param')
+       -> Node   -- ^ Term where variables may occur. (Cannot contain functions.)
        -> m Node
-forall = liftBoolector2 B.forall
+forall n1 n2 = mkNode ["forall", show n1, show n2] $  liftBoolector2 B.forall (map _node n1) (_node n2)
 
 -- | Create an existentially quantifed term.
 exists :: MonadBoolector m
-       => [Node] -- ^ Quantified variables
-       -> Node   -- ^ Term where variables may occur
+       => [Node] -- ^ Quantified variables (create with 'param')
+       -> Node   -- ^ Term where variables may occur. (Cannot contain functions.)
        -> m Node
-exists = liftBoolector2 B.exists
+exists n1 n2 = mkNode ["exists", show n1, show n2] $  liftBoolector2 B.exists (map _node n1) (_node n2)
 
 --
 -- Accessors
@@ -788,31 +834,31 @@
 
 -- | Get the sort of given @node@. The result does not have to be released.
 getSort :: MonadBoolector m => Node -> m Sort
-getSort = liftBoolector1 B.getSort
+getSort n = liftBoolector1 B.getSort (_node n) >>= lookupSort
 
 -- | Get the domain sort of given function node @node@.
 --
 -- The result does not have to be released.
 funGetDomainSort :: MonadBoolector m => Node -> m Sort
-funGetDomainSort = liftBoolector1 B.funGetDomainSort
+funGetDomainSort n = liftBoolector1 B.funGetDomainSort (_node n) >>= lookupSort
 
 -- | Get the codomain sort of given function node @node@.
 --
 -- The result does not have to be released.
 funGetCodomainSort :: MonadBoolector m => Node -> m Sort
-funGetCodomainSort = liftBoolector1 B.funGetCodomainSort
+funGetCodomainSort n = liftBoolector1 B.funGetCodomainSort (_node n) >>= lookupSort
 
 -- | Get the arity of function node.
 funGetArity :: MonadBoolector m => Node -> m Word
-funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity n
+funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity (_node n)
 
 -- | Get the symbol of an expression.
 getSymbol :: MonadBoolector m => Node -> m (Maybe String)
-getSymbol = liftBoolector1 B.getSymbol
+getSymbol = liftBoolector1 B.getSymbol . _node
 
 -- | Set the symbol of an expression.
 setSymbol :: MonadBoolector m => Node -> String -> m ()
-setSymbol = liftBoolector2 B.setSymbol
+setSymbol n str = liftBoolector2 B.setSymbol (_node n) str
 
 -- | Get the bit width of an expression.
 --
@@ -820,44 +866,44 @@
 -- elements.
 -- If the expression is a function, it returns the bit width of the function's
 -- return value.
-getWidth :: MonadBoolector m => Node -> m Word
-getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth n
+getWidth :: MonadBoolector m => Node -> m Word32
+getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth (_node n)
 
 -- | Get the bit width of indices of @n_array@.
-getIndexWidth :: MonadBoolector m => Node -> m Word
-getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth n
+getIndexWidth :: MonadBoolector m => Node -> m Word32
+getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth (_node n)
 
 -- | Determine if given node is a constant node.
 isConst :: MonadBoolector m => Node -> m Bool
-isConst = liftBoolector1 B.isConst
+isConst = liftBoolector1 B.isConst . _node
 
 -- | Determine if given node is a bit vector variable.
 isVar :: MonadBoolector m => Node -> m Bool
-isVar = liftBoolector1 B.isVar
+isVar = liftBoolector1 B.isVar . _node
 
 -- | Determine if given node is an array node.
 isArray :: MonadBoolector m => Node -> m Bool
-isArray = liftBoolector1 B.isArray
+isArray = liftBoolector1 B.isArray . _node
 
 -- | Determine if given node is an array node.
 isArrayVar :: MonadBoolector m => Node -> m Bool
-isArrayVar = liftBoolector1 B.isArrayVar
+isArrayVar = liftBoolector1 B.isArrayVar . _node
 
 -- | Determine if given node is a parameter node.
 isParam :: MonadBoolector m => Node -> m Bool
-isParam = liftBoolector1 B.isParam
+isParam = liftBoolector1 B.isParam . _node
 
 -- | Determine if given parameter node is bound by a function.
 isBoundParam :: MonadBoolector m => Node -> m Bool
-isBoundParam = liftBoolector1 B.isBoundParam
+isBoundParam = liftBoolector1 B.isBoundParam . _node
 
 -- | Determine if given node is an uninterpreted function node.
 isUf :: MonadBoolector m => Node -> m Bool
-isUf = liftBoolector1 B.isUf
+isUf = liftBoolector1 B.isUf . _node
 
 -- | Determine if given node is a function node.
 isFun :: MonadBoolector m => Node -> m Bool
-isFun = liftBoolector1 B.isFun
+isFun = liftBoolector1 B.isFun . _node
 
 
 --
@@ -872,7 +918,7 @@
 -- occurs in an assertion or current assumption. The assignment string has to
 -- be freed by 'freeBvAssignment'.
 bvAssignment :: MonadBoolector m => Node -> m String
-bvAssignment = liftBoolector1 B.bvAssignment
+bvAssignment = liftBoolector1 B.bvAssignment . _node
 
 -- | Get unsigned integer value from model.
 unsignedBvAssignment :: MonadBoolector m => Node -> m Integer
@@ -904,14 +950,28 @@
 -- Sorts
 --
 
+-- | Type of sorts, used to keep track of sorts without having to go back into C-land.
+data SortTy = BoolSort
+            | BitVecSort Word
+            | FunSort [SortTy] SortTy
+            | ArraySort SortTy SortTy
+            deriving (Eq, Ord, Show)
 
+-- | Sort wraps the udnerlying Boolector sort with a showable type.
+data Sort = Sort { sortTy :: SortTy -- ^ Get sort type
+                 , _sort  :: B.Sort
+                 } deriving (Eq, Ord)
+
+instance Show Sort where
+  show = show . sortTy
+
 -- | Create Boolean sort.
 boolSort :: Boolector Sort
 boolSort = do
   sc <- getSortCache
   case scBool sc of
     Just srt -> return srt
-    _ -> do srt <- liftBoolector0 B.boolSort
+    _ -> do srt <- Sort BoolSort <$> liftBoolector0 B.boolSort
             setSortCache $ sc { scBool = Just srt }
             return srt
 
@@ -922,7 +982,7 @@
   let bvMap = scBitVec sc
   case IntMap.lookup nr bvMap of
     Just srt -> return srt
-    _ -> do srt <- liftBoolector1 B.bitvecSort nr
+    _ -> do srt <- Sort (BitVecSort nr) <$> liftBoolector1 B.bitvecSort nr
             setSortCache $ sc { scBitVec = IntMap.insert nr srt bvMap }
             return srt
   where nr = fromIntegral wnr
@@ -934,7 +994,8 @@
   let funMap = scFun sc
   case Map.lookup (ret, args) funMap of
     Just srt -> return srt
-    _ -> do srt <- liftBoolector2 B.funSort args ret
+    _ -> do srt <- Sort (FunSort (map sortTy args) (sortTy ret))
+                       <$> liftBoolector2 B.funSort (map _sort args) (_sort ret)
             setSortCache $ sc { scFun = Map.insert (ret, args) srt funMap }
             return srt
 
@@ -945,31 +1006,38 @@
   let arrMap = scArray sc
   case Map.lookup (dom, rng) arrMap of
     Just srt -> return srt
-    _ -> do srt <- liftBoolector2 B.arraySort dom rng
+    _ -> do srt <- Sort (ArraySort (sortTy dom) (sortTy rng))
+                      <$> liftBoolector2 B.arraySort (_sort dom) (_sort rng)
             setSortCache $ sc { scArray = Map.insert (dom, rng) srt arrMap }
             return srt
 
 -- | Determine if @n0@ and @n1@ have the same sort or not.
 isEqualSort :: MonadBoolector m => Node -> Node -> m Bool
-isEqualSort = liftBoolector2 B.isEqualSort
+isEqualSort n1 n2 = liftBoolector2 B.isEqualSort (_node n1) (_node n2)
 
 -- | Determine if @sort@ is an array sort.
-isArraySort :: MonadBoolector m => Sort -> m Bool
-isArraySort = liftBoolector1 B.isArraySort
+isArraySort :: Sort -> Bool
+isArraySort srt = case sortTy srt of
+                    BitVecSort _ -> True
+                    _ -> False
 
 -- | Determine if @sort@ is a bit-vector sort.
-isBitvecSort :: MonadBoolector m => Sort -> m Bool
-isBitvecSort = liftBoolector1 B.isBitvecSort
+isBitvecSort :: Sort -> Bool
+isBitvecSort srt = case sortTy srt of
+                    ArraySort _ _ -> True
+                    _ -> False
 
 -- | Determine if @sort@ is a function sort.
-isFunSort :: MonadBoolector m => Sort -> m Bool
-isFunSort = liftBoolector1 B.isFunSort
+isFunSort :: Sort -> Bool
+isFunSort srt = case sortTy srt of
+                    FunSort _ _ -> True
+                    _ -> False
 
 -- | Check if sorts of given arguments matches the function signature.
 -- Returns 'Nothing' if all sorts are correct; otherwise it returns the
 -- position of the incorrect argument.
 funSortCheck :: MonadBoolector m => [Node] -> Node -> m (Maybe Int)
-funSortCheck = liftBoolector2 B.funSortCheck
+funSortCheck n1 n2 = liftBoolector2 B.funSortCheck (map _node n1) (_node n2)
 
 
 --
@@ -984,7 +1052,7 @@
 dumpNode :: MonadBoolector m => DumpFormat -> FilePath -> Node -> m ()
 dumpNode fmt path node = do
   btor <- unBoolectorState `liftM` getBoolectorState
-  liftIO $ B.withDumpFile path $ \file -> dumper btor file node
+  liftIO $ B.withDumpFile path $ \file -> dumper btor file (_node node)
   where dumper = case fmt of
                   DumpBtor -> B.dumpBtorNode
                   _        -> B.dumpSmt2Node
@@ -1003,7 +1071,7 @@
 dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String
 dumpNodeToString fmt node = do
   btor <- unBoolectorState `liftM` getBoolectorState
-  liftIO $ B.withTempDumpFile (\file -> dumper btor file node)
+  liftIO $ B.withTempDumpFile (\file -> dumper btor file (_node node))
   where dumper = case fmt of
                   DumpBtor -> B.dumpBtorNode
                   _        -> B.dumpSmt2Node
@@ -1091,15 +1159,59 @@
   s0 <- getBoolectorState
   putBoolectorState $ s0 { unBoolectorCache = (unBoolectorCache s0) { varCache = vc } }
 
+
+--
+-- Internal helpers
+--
+
+-- | Class used to create nodes from boolector nodes, given a stringification
+class Show s => MkNode s where
+  mkNode :: MonadBoolector m => s -> m B.Node -> m Node
+
+instance MkNode String where
+  mkNode str act = do
+    node <- act
+    return $ Node node str
+
+instance MkNode [String] where
+  mkNode str act = do
+    node <- act
+    return $ Node node $ "(" ++ unwords str ++ ")"
+
+
 -- | Create a new named node given a constructor or return it from variable
 -- cache. The name must be unique.
-createNamedNode :: MonadBoolector m
-                => (B.Btor -> Sort -> String -> IO Node)
-                -> Sort -> String -> m Node
-createNamedNode ctor sort name = do
+mkNamedNode :: MonadBoolector m
+            => String                                    -- ^ Kind of node
+            -> (B.Btor -> B.Sort -> String -> IO B.Node) -- ^ Underlying constructor
+            -> Sort                                      -- ^ Sort of node
+            -> String                                    -- ^ Name of node
+            -> m Node
+mkNamedNode kind ctor sort name = do
   vc <- getVarCache
   case Map.lookup (name, sort) vc of
     Just srt -> return srt
-    _ -> do node <- liftBoolector2 ctor sort name
+    _ -> do node <- mkNode [kind, name, "::", show sort] $
+                      liftBoolector2 ctor (_sort sort) name
             setVarCache $ Map.insert (name, sort) node vc
             return node
+
+-- | Get the high level sort from cache that corresponds to boolector sort
+lookupSort :: MonadBoolector m => B.Sort -> m Sort
+lookupSort bSort = do
+  sc <- getSortCache
+  case () of
+    _ | Just srt <- lookupBoolSort sc   -> return srt
+    _ | Just srt <- lookupBitVecSort sc -> return srt
+    _ | Just srt <- lookupFunSort sc    -> return srt
+    _ | Just srt <- lookupArraySort sc  -> return srt
+    _ -> fail "BUG: should really have the sort in the cache"
+  where lookupBoolSort sc = case scBool sc of
+                              Just srt | _sort srt == bSort -> Just srt
+                              _ -> Nothing
+        lookupBitVecSort sc = listToMaybe $ IntMap.elems $
+                                IntMap.filter (\s -> _sort s == bSort) $ scBitVec sc
+        lookupFunSort sc = listToMaybe $ Map.elems $
+                                Map.filter (\s -> _sort s == bSort) $ scFun sc
+        lookupArraySort sc = listToMaybe $ Map.elems $
+                                Map.filter (\s -> _sort s == bSort) $ scArray sc
diff --git a/test/API_Usage_Example.hs b/test/API_Usage_Example.hs
--- a/test/API_Usage_Example.hs
+++ b/test/API_Usage_Example.hs
@@ -24,10 +24,14 @@
     e  <- B.eq c p
 
     -- Make some assertions
-    B.assert =<< B.and no e
+    B.and no e >>= \node -> do
+      liftIO $ putStrLn (show node)
+      B.assert node
+
     one <- B.one u8
     B.assert =<< B.ugt x one
     B.assert =<< B.ugt y one
+
 
     -- Dump the corresponding SMT Lib 2 to a file
     B.dump B.DumpSMT2 "dump_example.smt2"
diff --git a/test/Arith_Example2.hs b/test/Arith_Example2.hs
new file mode 100644
--- /dev/null
+++ b/test/Arith_Example2.hs
@@ -0,0 +1,93 @@
+import qualified Boolector as B
+
+import Control.Monad.IO.Class
+import Control.Exception (assert)
+
+
+main :: IO ()
+main = do
+  bs <- B.newBoolectorState Nothing
+  B.evalBoolector bs $ do
+    -- Create sorts:
+    i64   <- B.bitvecSort 64
+    fSort <- B.funSort [i64] i64
+    gSort <- B.funSort [i64, i64] i64
+
+    -- Create variables x, y, z, f, g
+    x <- B.var i64 "x"
+    y <- B.var i64 "y"
+    z <- B.var i64 "z"
+    f <- B.uf fSort "f"
+    g <- B.uf gSort "g"
+
+    -- Create constant:
+    two <- B.signedInt (-2^60) i64
+    
+    -- Create action to print model
+    let printModel = do mx <- B.signedBvAssignment x
+                        my <- B.signedBvAssignment y
+                        mz <- B.signedBvAssignment z
+                        liftIO $ putStrLn $ show [mx, my, mz]
+  
+    -- (assert (>= (* -2^60 x) (+ y z)))
+    do tmp1 <- B.mul two x
+       tmp2 <- B.add y z
+       tmp2Str <- B.dumpNodeToString B.DumpSMT2 tmp2
+       liftIO $ putStrLn $ "tmp2Str = " ++ tmp2Str
+       B.assert =<< B.sgte tmp1 tmp2
+
+    -- (assert (< (f x) (g x x)))
+    do tmp1 <- B.apply [x] f
+       tmp2 <- B.apply [x, x] g
+       B.assert =<< B.slt tmp1 tmp2
+
+    -- (assert (> (f y) (g x x)))
+    do tmp1 <- B.apply [y] f
+       tmp2 <- B.apply [x, x] g
+       B.assert =<< B.sgt tmp1 tmp2
+
+    -- Check satisfiability:
+    B.Sat <- B.sat
+
+    -- Print model:
+    printModel
+
+    -- Push context
+    B.push 1
+
+    -- Add (false) assertion:
+    B.assert =<< B.eq x y
+
+    -- Check satisfiability:
+    B.Unsat <- B.sat
+
+    -- Pop context
+    B.pop 1
+
+    -- Can check sat again and pirnt model
+    B.Sat <- B.sat
+    printModel
+
+
+
+{- This example is from https://rise4fun.com/Z3/smtc_arith:
+
+; This example illustrates basic arithmetic and uninterpreted functions
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(assert (>= (* 2 x) (+ y z)))
+(declare-fun f (Int) Int)
+(declare-fun g (Int Int) Int)
+(assert (< (f x) (g x x)))
+(assert (> (f y) (g x x)))
+(check-sat)
+(get-model)
+(push)
+(assert (= x y))
+(check-sat)
+(pop)
+(exit)
+
+-}
+
diff --git a/test/UF_Example2.hs b/test/UF_Example2.hs
new file mode 100644
--- /dev/null
+++ b/test/UF_Example2.hs
@@ -0,0 +1,40 @@
+import qualified Boolector as B
+import Control.Monad.IO.Class
+
+main :: IO ()
+main = do
+  bs <- B.newBoolectorState Nothing
+  B.evalBoolector bs $ do
+    -- Create sorts:
+    i32   <- B.bitvecSort 32
+    fSort <- B.funSort [i32] i32
+    
+    -- Create constants:
+    one   <- B.signedInt 1 i32
+    two   <- B.signedInt 2 i32
+    five  <- B.signedInt 5 i32
+    fifty <- B.signedInt 50 i32
+
+    -- Create variable and function:
+    x <- B.var i32 "x"
+    f <- B.uf fSort "f"
+
+    -- f(x) >= 5 && f(x) < 50
+    do tmp1 <- B.apply [x] f 
+       B.assert =<< B.sgte tmp1 five
+       B.assert =<< B.slt tmp1 fifty
+
+    -- f(2) + 1 > 5 && f(2) <= 50
+    do tmp1 <- B.apply [two] f
+       tmp2 <- B.add tmp1 one
+       B.assert =<< B.sgte tmp2 five
+       B.assert =<< B.slte tmp2 fifty
+
+    -- x >= 2
+    B.assert =<< B.sgte x two
+
+    -- Check satisfiability:
+    B.Sat <- B.sat
+
+    return ()
+