diff --git a/Data/SBV.hs b/Data/SBV.hs
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -15,14 +15,13 @@
 -- Express properties about bit-precise Haskell programs and automatically prove
 -- them using SMT solvers.
 --
--- >   $ ghci -XScopedTypeVariables
--- >   Prelude> :m Data.SBV
--- >   Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
--- >   Q.E.D.
--- >   Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
--- >   Falsifiable. Counter-example:
--- >     x = 128 :: SWord8
+-- >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
+-- Q.E.D.
 --
+-- >>> prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8)
+-- Falsifiable. Counter-example:
+--   x = 128 :: SWord8
+--
 -- The function 'prove' has the following type:
 --
 -- @
@@ -129,6 +128,10 @@
   , PrettyNum(..), readBin
   -- * Uninterpreted constants and functions
   , Uninterpreted(..)
+  -- ** Accessing the handle
+  , SBVUF, sbvUFName
+  -- ** Adding axioms
+  , addAxiom
 
   -- * Proving properties
   -- $proveIntro
diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs
--- a/Data/SBV/BitVectors/Data.hs
+++ b/Data/SBV/BitVectors/Data.hs
@@ -31,7 +31,7 @@
  , SBVExpr(..), newExpr
  , cache, uncache, HasSignAndSize(..)
  , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, State, Size, output, Result(..)
- , SBVType(..), newUninterpreted, unintFnUIKind
+ , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom
  ) where
 
 import Control.DeepSeq                 (NFData(..))
@@ -243,14 +243,15 @@
                      [((Int, Int, Int), [SW])]     -- tables (automatically constructed)
                      [(Int, ArrayInfo)]            -- arrays (user specified)
                      [(String, SBVType)]           -- uninterpreted constants
+                     [(String, [String])]          -- axioms
                      Pgm                           -- assignments
                      [SW]                          -- outputs
 
 instance Show Result where
-  show (Result _ cs _ _ [] _ [r])
+  show (Result _ cs _ _ [] [] _ [r])
     | Just c <- r `lookup` cs
     = show c
-  show (Result is cs ts as uis xs os)  = intercalate "\n" $
+  show (Result is cs ts as uis axs xs os)  = intercalate "\n" $
                    ["INPUTS"]
                 ++ map shn is
                 ++ ["CONSTANTS"]
@@ -261,6 +262,8 @@
                 ++ map sha as
                 ++ ["UNINTERPRETED CONSTANTS"]
                 ++ map shui uis
+                ++ ["AXIOMS"]
+                ++ map shax axs
                 ++ ["DEFINE"]
                 ++ map (\(s, e) -> "  " ++ shs s ++ " = " ++ show e) (F.toList xs)
                 ++ ["OUTPUTS"]
@@ -281,6 +284,7 @@
                   alias | ni == nm = ""
                         | True     = ", aliasing " ++ show nm
           shui (nm, t) = "  uninterpreted_" ++ nm ++ " :: " ++ show t
+          shax (nm, ss) = "  -- user defined axiom: " ++ nm ++ "\n  " ++ intercalate "\n  " ss
 
 data ArrayContext = ArrayFree (Maybe SW)
                   | ArrayReset Int SW
@@ -323,6 +327,7 @@
                     , rexprMap   :: IORef ExprMap
                     , rArrayMap  :: IORef ArrayMap
                     , rUIMap     :: IORef UIMap
+                    , raxioms    :: IORef [(String, [String])]
                     }
 
 -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic
@@ -478,6 +483,14 @@
         liftIO $ modifyIORef (routs st) (sw:)
         return i
 
+-- | Add a user specified axiom to the generated SMT-Lib file. Note that the input is a
+-- mere string; we perform no checking on the input that it's well-formed or is sensical.
+-- A separate formalization of SMT-Lib would be very useful here.
+addAxiom :: String -> [String] -> Symbolic ()
+addAxiom nm ax = do
+        st <- ask
+        liftIO $ modifyIORef (raxioms st) ((nm, ax) :)
+
 -- | Run a symbolic computation and return a 'Result'
 runSymbolic :: Symbolic a -> IO Result
 runSymbolic (Symbolic c) = do
@@ -490,6 +503,7 @@
    tables <- newIORef Map.empty
    arrays <- newIORef IMap.empty
    uis    <- newIORef Map.empty
+   axioms <- newIORef []
    let st = State { rctr      = ctr
                   , rinps     = inps
                   , routs     = outs
@@ -499,6 +513,7 @@
                   , rArrayMap = arrays
                   , rexprMap  = emap
                   , rUIMap    = uis
+                  , raxioms   = axioms
                   }
    _ <- newConst st $ W1 Zero -- s(-2) == falseSW
    _ <- newConst st $ W1 One  -- s(-1) == trueSW
@@ -512,7 +527,8 @@
    tbls  <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef tables
    arrs  <- IMap.toAscList `fmap` readIORef arrays
    unint <- Map.toList `fmap` readIORef uis
-   return $ Result (reverse inpsR) cnsts tbls arrs unint rpgm (reverse outsR)
+   axs   <- reverse `fmap` readIORef axioms
+   return $ Result (reverse inpsR) cnsts tbls arrs unint axs rpgm (reverse outsR)
 
 -------------------------------------------------------------------------------
 -- * Symbolic Words
@@ -704,7 +720,8 @@
   rnf (I64 w) = rnf w `seq` ()
 
 instance NFData Result where
-  rnf (Result inps consts tbls arrs uis pgm outs) = rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf pgm `seq` rnf outs
+  rnf (Result inps consts tbls arrs uis axs pgm outs)
+        = rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf outs
 
 instance NFData ArrayContext
 instance NFData Pgm
diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs
--- a/Data/SBV/BitVectors/Model.hs
+++ b/Data/SBV/BitVectors/Model.hs
@@ -22,7 +22,7 @@
 module Data.SBV.BitVectors.Model (
     Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..)
   , bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE
-  , lsb, msb
+  , lsb, msb, SBVUF, sbvUFName
   )
   where
 
@@ -635,23 +635,45 @@
 instance SymWord b => Mergeable (SFunArray a b) where
   symbolicMerge = mergeArrays
 
+-- | An uninterpreted function handle. This is the handle to be used for
+-- adding axioms about uninterpreted constants/functions. Note that
+-- we will leave this abstract for safety purposes
+newtype SBVUF = SBVUF String
+
+-- | Get the name associated with the uninterpreted-value; useful when
+-- constructing axioms about this UI.
+sbvUFName :: SBVUF -> String
+sbvUFName (SBVUF s) = s
+
+-- The name we use for translating the UF constants to SMT-Lib..
+mkUFName :: String -> SBVUF
+mkUFName nm = SBVUF $ "uninterpreted_" ++ nm
+
 -- | Uninterpreted constants and functions. An uninterpreted constant is
 -- a value that is indexed by its name. The only property the prover assumes
 -- about these values are that they are equivalent to themselves; i.e., (for
 -- functions) they return the same results when applied to same arguments.
 -- We support uninterpreted-functions as a general means of black-box'ing
--- operations that are "irrelevant" for the purposes of the proof; i.e., when
+-- operations that are /irrelevant/ for the purposes of the proof; i.e., when
 -- the proofs can be performed without any knowledge about the function itself.
 --
--- Minimal complete definition: 'uninterpret'. However, most instances in
+-- Minimal complete definition: 'uninterpretWithHandle'. However, most instances in
 -- practice are already provided by SBV, so end-users should not need to define their
 -- own instances.
 class Uninterpreted a where
+  -- | Uninterpret a value, receiving an object that can be used instead. Use this version
+  -- when you do not need to add an axiom about this value.
   uninterpret :: String -> a
+  -- | Uninterpret a value, but also get a handle to the resulting object. This handle
+  -- can be used to add axioms for this object. (See 'addAxiom'.)
+  uninterpretWithHandle :: String -> (SBVUF, a)
 
+  -- minimal complete definition: 'uninterpretWithHandle'
+  uninterpret = snd . uninterpretWithHandle
+
 -- Plain constants
 instance HasSignAndSize a => Uninterpreted (SBV a) where
-  uninterpret nm = SBV sgnsza $ Right $ cache result
+  uninterpretWithHandle nm = (mkUFName nm, SBV sgnsza $ Right $ cache result)
     where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
           result st = do newUninterpreted st nm (SBVType [sgnsza])
                          newExpr st sgnsza $ SBVApp (Uninterpreted nm) []
@@ -664,144 +686,151 @@
 
 -- Functions of one argument
 instance (HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) where
-  uninterpret nm arg0 = SBV sgnsza $ Right $ cache result
-    where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
-          sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
-          result st = do newUninterpreted st nm (SBVType [sgnszb, sgnsza])
-                         sw0 <- sbvToSW st arg0
-                         mapM_ forceArg [sw0]
-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]
+  uninterpretWithHandle nm = (mkUFName nm, f)
+    where f arg0 = SBV sgnsza $ Right $ cache result
+           where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
+                 sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
+                 result st = do newUninterpreted st nm (SBVType [sgnszb, sgnsza])
+                                sw0 <- sbvToSW st arg0
+                                mapM_ forceArg [sw0]
+                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]
 
 -- Functions of two arguments
 instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) where
-  uninterpret nm arg0 arg1 = SBV sgnsza $ Right $ cache result
-    where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
-          sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
-          sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
-          result st = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza])
-                         sw0 <- sbvToSW st arg0
-                         sw1 <- sbvToSW st arg1
-                         mapM_ forceArg [sw0, sw1]
-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]
+  uninterpretWithHandle nm = (mkUFName nm, f)
+    where f arg0 arg1 = SBV sgnsza $ Right $ cache result
+           where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
+                 sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
+                 sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
+                 result st = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza])
+                                sw0 <- sbvToSW st arg0
+                                sw1 <- sbvToSW st arg1
+                                mapM_ forceArg [sw0, sw1]
+                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]
 
 -- Functions of three arguments
 instance (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where
-  uninterpret nm arg0 arg1 arg2 = SBV sgnsza $ Right $ cache result
-    where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
-          sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
-          sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
-          sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
-          result st = do newUninterpreted st nm (SBVType [sgnszd, sgnszc, sgnszb, sgnsza])
-                         sw0 <- sbvToSW st arg0
-                         sw1 <- sbvToSW st arg1
-                         sw2 <- sbvToSW st arg2
-                         mapM_ forceArg [sw0, sw1, sw2]
-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]
+  uninterpretWithHandle nm = (mkUFName nm, f)
+    where f arg0 arg1 arg2 = SBV sgnsza $ Right $ cache result
+           where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
+                 sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
+                 sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
+                 sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
+                 result st = do newUninterpreted st nm (SBVType [sgnszd, sgnszc, sgnszb, sgnsza])
+                                sw0 <- sbvToSW st arg0
+                                sw1 <- sbvToSW st arg1
+                                sw2 <- sbvToSW st arg2
+                                mapM_ forceArg [sw0, sw1, sw2]
+                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]
 
 -- Functions of four arguments
 instance (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
-  uninterpret nm arg0 arg1 arg2 arg3 = SBV sgnsza $ Right $ cache result
-    where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
-          sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
-          sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
-          sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
-          sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
-          result st = do newUninterpreted st nm (SBVType [sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
-                         sw0 <- sbvToSW st arg0
-                         sw1 <- sbvToSW st arg1
-                         sw2 <- sbvToSW st arg2
-                         sw3 <- sbvToSW st arg3
-                         mapM_ forceArg [sw0, sw1, sw2, sw3]
-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]
+  uninterpretWithHandle nm = (mkUFName nm, f)
+    where f arg0 arg1 arg2 arg3 = SBV sgnsza $ Right $ cache result
+           where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
+                 sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
+                 sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
+                 sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
+                 sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
+                 result st = do newUninterpreted st nm (SBVType [sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
+                                sw0 <- sbvToSW st arg0
+                                sw1 <- sbvToSW st arg1
+                                sw2 <- sbvToSW st arg2
+                                sw3 <- sbvToSW st arg3
+                                mapM_ forceArg [sw0, sw1, sw2, sw3]
+                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]
 
 -- Functions of five arguments
 instance (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
-  uninterpret nm arg0 arg1 arg2 arg3 arg4 = SBV sgnsza $ Right $ cache result
-    where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
-          sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
-          sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
-          sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
-          sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
-          sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
-          result st = do newUninterpreted st nm (SBVType [sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
-                         sw0 <- sbvToSW st arg0
-                         sw1 <- sbvToSW st arg1
-                         sw2 <- sbvToSW st arg2
-                         sw3 <- sbvToSW st arg3
-                         sw4 <- sbvToSW st arg4
-                         mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]
-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]
+  uninterpretWithHandle nm = (mkUFName nm, f)
+    where f arg0 arg1 arg2 arg3 arg4 = SBV sgnsza $ Right $ cache result
+           where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
+                 sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
+                 sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
+                 sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
+                 sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
+                 sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
+                 result st = do newUninterpreted st nm (SBVType [sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
+                                sw0 <- sbvToSW st arg0
+                                sw1 <- sbvToSW st arg1
+                                sw2 <- sbvToSW st arg2
+                                sw3 <- sbvToSW st arg3
+                                sw4 <- sbvToSW st arg4
+                                mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]
+                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]
 
 -- Functions of six arguments
 instance (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
-  uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5 = SBV sgnsza $ Right $ cache result
-    where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
-          sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
-          sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
-          sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
-          sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
-          sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
-          sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))
-          result st = do newUninterpreted st nm (SBVType [sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
-                         sw0 <- sbvToSW st arg0
-                         sw1 <- sbvToSW st arg1
-                         sw2 <- sbvToSW st arg2
-                         sw3 <- sbvToSW st arg3
-                         sw4 <- sbvToSW st arg4
-                         sw5 <- sbvToSW st arg5
-                         mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]
-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]
+  uninterpretWithHandle nm = (mkUFName nm, f)
+    where f arg0 arg1 arg2 arg3 arg4 arg5 = SBV sgnsza $ Right $ cache result
+           where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
+                 sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
+                 sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
+                 sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
+                 sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
+                 sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
+                 sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))
+                 result st = do newUninterpreted st nm (SBVType [sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
+                                sw0 <- sbvToSW st arg0
+                                sw1 <- sbvToSW st arg1
+                                sw2 <- sbvToSW st arg2
+                                sw3 <- sbvToSW st arg3
+                                sw4 <- sbvToSW st arg4
+                                sw5 <- sbvToSW st arg5
+                                mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]
+                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]
 
 -- Functions of seven arguments
 instance (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where
-  uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5 arg6 = SBV sgnsza $ Right $ cache result
-    where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
-          sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
-          sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
-          sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
-          sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
-          sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
-          sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))
-          sgnszh = (hasSign (undefined :: h), sizeOf (undefined :: h))
-          result st = do newUninterpreted st nm (SBVType [sgnszh, sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
-                         sw0 <- sbvToSW st arg0
-                         sw1 <- sbvToSW st arg1
-                         sw2 <- sbvToSW st arg2
-                         sw3 <- sbvToSW st arg3
-                         sw4 <- sbvToSW st arg4
-                         sw5 <- sbvToSW st arg5
-                         sw6 <- sbvToSW st arg6
-                         mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
-                         newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
+  uninterpretWithHandle nm = (mkUFName nm, f)
+    where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 = SBV sgnsza $ Right $ cache result
+           where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))
+                 sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))
+                 sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))
+                 sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))
+                 sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))
+                 sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))
+                 sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))
+                 sgnszh = (hasSign (undefined :: h), sizeOf (undefined :: h))
+                 result st = do newUninterpreted st nm (SBVType [sgnszh, sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])
+                                sw0 <- sbvToSW st arg0
+                                sw1 <- sbvToSW st arg1
+                                sw2 <- sbvToSW st arg2
+                                sw3 <- sbvToSW st arg3
+                                sw4 <- sbvToSW st arg4
+                                sw5 <- sbvToSW st arg5
+                                sw6 <- sbvToSW st arg6
+                                mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
+                                newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]
 
 -- Uncurried functions of two arguments
 instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where
-  uninterpret nm (arg0, arg1) = uninterpret nm arg0 arg1
+  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1) -> f arg0 arg1)
 
 -- Uncurried functions of three arguments
 instance (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where
-  uninterpret nm (arg0, arg1, arg2) = uninterpret nm arg0 arg1 arg2
+  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2) -> f arg0 arg1 arg2)
 
 -- Uncurried functions of four arguments
 instance (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where
-  uninterpret nm (arg0, arg1, arg2, arg3) = uninterpret nm arg0 arg1 arg2 arg3
+  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3)
 
 -- Uncurried functions of five arguments
 instance (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
-  uninterpret nm (arg0, arg1, arg2, arg3, arg4) = uninterpret nm arg0 arg1 arg2 arg3 arg4
+  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4)
 
 -- Uncurried functions of six arguments
 instance (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
-  uninterpret nm (arg0, arg1, arg2, arg3, arg4, arg5) = uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5
+  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5)
 
 -- Uncurried functions of seven arguments
 instance (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)
             => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
-  uninterpret nm (arg0, arg1, arg2, arg3, arg4, arg5, arg6) = uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5 arg6
+  uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6)
diff --git a/Data/SBV/Examples/PrefixSum/PrefixSum.hs b/Data/SBV/Examples/PrefixSum/PrefixSum.hs
--- a/Data/SBV/Examples/PrefixSum/PrefixSum.hs
+++ b/Data/SBV/Examples/PrefixSum/PrefixSum.hs
@@ -20,6 +20,10 @@
 
 import Data.SBV
 
+----------------------------------------------------------------------
+-- * Formalizing power-lists
+----------------------------------------------------------------------
+
 -- | A poor man's representation of powerlists and
 -- basic operations on them: <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.
 -- We merely represent power-lists by ordinary lists.
@@ -43,10 +47,18 @@
         chunk2 (x:y:xs) = (x,y) : chunk2 xs
         chunk2 _        = error "unzipPL: malformed powerlist"
 
+----------------------------------------------------------------------
+-- * Reference prefix-sum implementation
+----------------------------------------------------------------------
+
 -- | Reference prefix sum (@ps@) is simply Haskell's @scanl1@ function
 ps :: (a, a -> a -> a) -> PowerList a -> PowerList a
 ps (_, f) = scanl1 f
 
+----------------------------------------------------------------------
+-- * The Ladner-Fischer parallel version
+----------------------------------------------------------------------
+
 -- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>
 -- or pg. 16 of <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.
 lf :: (a, a -> a -> a) -> PowerList a -> PowerList a
@@ -58,18 +70,140 @@
          flpq   = lf (zero, f) pq
          rsh xs = zero : init xs
 
--- | Correctness theorem, for a powerlist of given size, an associative operator, and its unit element
+
+----------------------------------------------------------------------
+-- * Sample proofs for concrete operators
+----------------------------------------------------------------------
+
+-- | Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element
 flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
 flIsCorrect n zf = do
         args :: PowerList SWord32 <- mapM (const free_) [1..n]
         output $ ps zf args .== lf zf args
 
 -- | Proves Ladner-Fischer is equivalent to reference specification for addition.
--- @0@ is the unit element, and we use a power-list of size @8@.
+-- @0@ is the left-unit element, and we use a power-list of size @8@.
 thm1 :: IO ThmResult
 thm1 = prove $ flIsCorrect  8 (0, (+))
 
 -- | Proves Ladner-Fischer is equivalent to reference specification for the function @max@.
--- @0@ is the unit element, and we use a power-list of size @16@.
+-- @0@ is the left-unit element, and we use a power-list of size @16@.
 thm2 :: IO ThmResult
 thm2 = prove $ flIsCorrect 16 (0, smax)
+
+----------------------------------------------------------------------
+-- * Attempt at proving for arbitrary operators
+----------------------------------------------------------------------
+-- | Try proving correctness for an arbitrary operator. This proof will /not/ go through since the
+-- SMT solver does not know that the operator associative and has the given left-unit element
+--
+-- >>> thm3
+-- Falsifiable. Counter-example:
+--   s0 = 0 :: SWord32
+--   s1 = 0 :: SWord32
+--   s2 = 0 :: SWord32
+--   s3 = 0 :: SWord32
+--   s4 = 0 :: SWord32
+--   s5 = 0 :: SWord32
+--   s6 = 0 :: SWord32
+--   s7 = 3221225472 :: SWord32
+--   -- uninterpreted: u
+--        u  = 0
+--   -- uninterpreted: flOp
+--        flOp 0 3221225472 = 2147483648
+--        flOp 0 2147483648 = 3758096384
+--        flOp _ _          = 0
+--
+-- You can verify that the above function for @flOp@ is not associative:
+--
+-- @
+--   ghci> flOp 3221225472 (flOp 2147483648 3221225472)
+--   0
+--   ghci> flOp (flOp 3221225472 2147483648) 3221225472
+--   2147483648
+-- @
+--
+-- Also, the unit @0@ is clearly not a left-unit for @flOp@, as the third
+-- equation for @flOp@ will simply map many elements to @0@.
+thm3 :: IO ThmResult
+thm3 = prove $ do args :: PowerList SWord32 <- mapM (const free_) [(1::Int)..8]
+                  output $ ps (u, op) args .== lf (u, op) args
+  where op :: SWord32 -> SWord32 -> SWord32
+        op = uninterpret "flOp"
+        u :: SWord32
+        u = uninterpret "u"
+
+----------------------------------------------------------------------
+-- * Proving for arbitrary operators using axioms
+----------------------------------------------------------------------
+-- | Generate an instance of the prefix-sum problem for an arbitrary operator, by telling the SMT solver
+-- the necessary axioms for associativity and left-unit. The first argument states how wide the power list should be.
+genPrefixSumInstance :: Int -> Symbolic SBool
+genPrefixSumInstance n = do
+     args :: PowerList SWord32 <- mapM (const free_) [1..n]
+     addAxiom "flOp is associative"     $ assocAxiom (sbvUFName opH)
+     addAxiom "u is left-unit for flOp" $ leftUnitAxiom (sbvUFName opH) (sbvUFName uH)
+     output $ ps (u, op) args .== lf (u, op) args
+  where op :: SWord32 -> SWord32 -> SWord32
+        opH :: SBVUF
+        (opH, op) = uninterpretWithHandle "flOp"
+        u  :: SWord32
+        uH :: SBVUF
+        (uH, u)  = uninterpretWithHandle "u"
+        -- this is the brittle part; but it'll have to do until we get a proper
+        -- DSL for expressing SMT-axioms..
+        mkCall :: String -> String -> String -> String
+        mkCall o x y = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"
+        assocAxiom :: String -> [String]
+        assocAxiom o = [
+             ":assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])"
+           , "                    (= " ++ lhs
+           , "                       " ++ rhs
+           , "                    )"
+           , "            )"
+          ]
+          where lhs = mkCall o (mkCall o "?x" "?y") "?z"
+                rhs = mkCall o "?x" (mkCall o "?y" "?z")
+        leftUnitAxiom :: String -> String -> [String]
+        leftUnitAxiom o ue = [
+            ":assumption (forall (?x BitVec[32])"
+          , "                    (= " ++ lhs
+          , "                       " ++ rhs
+          , "                    )"
+          , "            )"
+          ]
+          where lhs = "(" ++ o ++ " " ++ ue ++ " " ++ "?x" ++ ")"
+                rhs = "?x"
+
+-- | Prove the generic problem for powerlists of given sizes. Note that
+-- this will only work for Yices-1. This is due to the fact that Yices-2
+-- follows the SMT-Lib standard and does not accept bit-vector problems with
+-- quantified axioms in them, while Yices-1 did allow for that. The crux of
+-- the problem is that there are no SMT-Lib logics that combine BV's and
+-- quantifiers, see: <http://goedel.cs.uiowa.edu/smtlib/logics.html>. So we
+-- are stuck until new powerful logics are added to SMT-Lib.
+--
+-- Here, we explicitly tell SBV to use Yices-1 that did not have that limitation.
+-- Tweak the executable location accordingly below for your platform..
+--
+-- We have:
+--
+-- >>> prefixSum 2
+-- Q.E.D.
+--
+-- >>> prefixSum 4
+-- Q.E.D.
+--
+-- Note that these proofs tend to run long. Also, Yices-1.0.28 ran out of memory
+-- and crashed on my box when I tried for size @8@, after running for about 2.5 minutes..
+prefixSum :: Int -> IO ThmResult
+prefixSum i
+  -- Fast way of checking whether a number is a power of two, see: <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>
+  | i <= 1 || (i .&. (i-1)) /= 0
+  = error $ "prefixSum: input must be a power of 2 larger than 2, received: " ++ show i
+  | True
+  = proveWith cfg $ genPrefixSumInstance i
+  where cfg = defaultSMTCfg { solver = yices' }
+        yices' = yices { options    = ["-tc", "-smt", "-e"]
+                       , executable = "/usr/local/yices-1.0.28/bin/yices"
+                       }
diff --git a/Data/SBV/Examples/Puzzles/DogCatMouse.hs b/Data/SBV/Examples/Puzzles/DogCatMouse.hs
--- a/Data/SBV/Examples/Puzzles/DogCatMouse.hs
+++ b/Data/SBV/Examples/Puzzles/DogCatMouse.hs
@@ -30,12 +30,12 @@
     &&&  dog + cat + mouse .== 100                     -- buy precisely 100 animals
     &&&  1500 * dog + 100 * cat + 25 * mouse .== 10000 -- spend exactly 100 dollars (use cents since we don't have fractions)
 
--- | prints the only solution:
+-- | Prints the only solution:
 --
--- @
---     dog = 3 :: SWord16
---     cat = 41 :: SWord16
---     mouse = 56 :: SWord16
--- @
-solve :: IO ()
-solve = print =<< allSat (forAll ["dog", "cat", "mouse"] puzzle)
+-- >>> solve
+-- Only one solution found:
+--   dog = 3 :: SWord16
+--   cat = 41 :: SWord16
+--   mouse = 56 :: SWord16
+solve :: IO AllSatResult
+solve = allSat $ forAll ["dog", "cat", "mouse"] puzzle
diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs
--- a/Data/SBV/Examples/Puzzles/U2Bridge.hs
+++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs
@@ -239,9 +239,9 @@
                shL True  = " <-- "
 
 -- | Solve the U2-bridge crossing puzzle, starting by testing solutions with
--- increasing number of steps, until we find one. This call prints:
+-- increasing number of steps, until we find one. We have:
 --
--- @
+-- >>> solveU2
 -- Checking for solutions with 1 move.
 -- Checking for solutions with 2 moves.
 -- Checking for solutions with 3 moves.
@@ -261,8 +261,7 @@
 -- 13 <-- Edge
 -- 15 --> Edge, Bono
 -- Total time: 17
--- Found: 2 solutions with 5 moves
--- @
+-- Found: 2 solutions with 5 moves.
 --
 -- Finding the all 2 possible solutions to the puzzle.
 solveU2 :: IO ()
diff --git a/Data/SBV/Examples/Uninterpreted/AUF.hs b/Data/SBV/Examples/Uninterpreted/AUF.hs
--- a/Data/SBV/Examples/Uninterpreted/AUF.hs
+++ b/Data/SBV/Examples/Uninterpreted/AUF.hs
@@ -32,8 +32,14 @@
 
 import Data.SBV
 
+--------------------------------------------------------------
+-- * Model using functional arrays
+--------------------------------------------------------------
+
 -- | The array type, takes symbolic 32-bit unsigned indexes
--- and stores 32-bit unsigned symbolic values
+-- and stores 32-bit unsigned symbolic values. These are
+-- functional arrays where reading before writing a cell
+-- throws an exception.
 type A = SFunArray Word32 Word32
 
 -- | Uninterpreted function in the theorem
@@ -42,13 +48,38 @@
 
 -- | Correctness theorem. We state it for all values of @x@, @y@, and 
 -- the array @a@. We also take an arbitrary initializer for the array.
-thm :: SWord32 -> SWord32 -> A -> SWord32 -> SBool
-thm x y a initVal = lhs ==> rhs
+thm1 :: SWord32 -> SWord32 -> A -> SWord32 -> SBool
+thm1 x y a initVal = lhs ==> rhs
   where a'  = resetArray a initVal -- initialize array
         lhs = x + 2 .== y
         rhs =     f (readArray (writeArray a' x 3) (y - 2))
               .== f (y - x + 1)
 
 -- | Prints Q.E.D. when run, as expected
-proveThm :: IO ()
-proveThm = print =<< prove thm
+--
+-- >>> proveThm1
+-- Q.E.D.
+proveThm1 :: IO ()
+proveThm1 = print =<< prove thm1
+
+--------------------------------------------------------------
+-- * Model using SMT arrays
+--------------------------------------------------------------
+
+-- | This version directly uses SMT-arrays and hence does not need an initializer.
+-- Reading an element before writing to it returns an arbitrary value.
+type B = SArray Word32 Word32
+
+-- | Same as 'thm1', except we don't need an initializer with the 'SArray' model.
+thm2 :: SWord32 -> SWord32 -> B -> SBool
+thm2 x y a = lhs ==> rhs
+  where lhs = x + 2 .== y
+        rhs =     f (readArray (writeArray a x 3) (y - 2))
+              .== f (y - x + 1)
+
+-- | Prints Q.E.D. when run, as expected:
+--
+-- >>> proveThm2
+-- Q.E.D.
+proveThm2 :: IO ()
+proveThm2 = print =<< prove thm2
diff --git a/Data/SBV/Examples/Uninterpreted/Function.hs b/Data/SBV/Examples/Uninterpreted/Function.hs
--- a/Data/SBV/Examples/Uninterpreted/Function.hs
+++ b/Data/SBV/Examples/Uninterpreted/Function.hs
@@ -26,15 +26,14 @@
 -- Indeed, the SMT solver (Yices in this case) returns a counter-example
 -- function that is not commutative. We have:
 --
--- @
--- ghci> prove $ forAll ["x", "y"] thmBad
+--
+-- >>> prove $ forAll ["x", "y"] thmBad
 -- Falsifiable. Counter-example:
 --   x = 0 :: SWord8
 --   y = 128 :: SWord8
 --   -- uninterpreted: f
 --        f 128 0 = 32768
 --        f _   _ = 0
--- @
 --
 -- Note how the counterexample function @f@ returned by Yices violates commutativity;
 -- thus providing evidence that the asserted theorem is not valid.
diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs
--- a/Data/SBV/Provers/Prover.hs
+++ b/Data/SBV/Provers/Prover.hs
@@ -287,9 +287,9 @@
         msg $ "Generated symbolic trace:\n" ++ show res
         msg "Translating to SMT-Lib.."
         case res of
-          Result is consts tbls arrs uis pgm [o@(SW{})] ->
+          Result is consts tbls arrs uis axs pgm [o@(SW{})] ->
              timeIf isTiming "translation" $ let uiMap = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis
-                                             in return (is, uiMap, toSMTLib isSat is consts tbls arrs uis pgm o)
+                                             in return (is, uiMap, toSMTLib isSat is consts tbls arrs uis axs pgm o)
           _ -> error $ "SBVProver.callSolver: Impossible happened: " ++ show res
 
 -- | Equality as a proof method. Allows for
diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs
--- a/Data/SBV/SMT/SMT.hs
+++ b/Data/SBV/SMT/SMT.hs
@@ -106,13 +106,15 @@
 
 instance Show AllSatResult where
   show (AllSatResult [])  =  "No solutions found"
-  show (AllSatResult [s]) =  "One solution found\n" ++ show (SatResult s)
-  show (AllSatResult ss)  =  "Multiple solutions found:\n"       -- shouldn't display how-many; would be too slow/leak-space to compute everything..
+  show (AllSatResult [s]) =  "Only one solution found:\n" ++ shUnique s
+        where shUnique = showSMTResult "Unsatisfiable"
+                                       ("Unknown (No assignment to variables returned)") "Unknown. Potential assignment:\n" "" ""
+  show (AllSatResult ss)  =  "Multiple solutions found:\n"      -- shouldn't display how-many; would be too slow/leak-space to compute everything..
                           ++ unlines (zipWith sh [(1::Int)..] ss)
                           ++ "Done."
-        where sh i s = showSMTResult "Unsatisfiable"
-                                     ("Unknown #" ++ show i ++ "(No assignment to variables returned)") "Unknown. Potential assignment:\n"
-                                     ("Solution #" ++ show i ++ " (No assignment to variables returned)") ("Solution #" ++ show i ++ ":\n") s
+        where sh i = showSMTResult "Unsatisfiable"
+                                   ("Unknown #" ++ show i ++ "(No assignment to variables returned)") "Unknown. Potential assignment:\n"
+                                   ("Solution #" ++ show i ++ " (No assignment to variables returned)") ("Solution #" ++ show i ++ ":\n")
 
 -- | Instances of 'SatModel' can be automatically extracted from models returned by the
 -- solvers. The idea is that the sbv infrastructure provides a stream of 'CW''s (constant-words)
@@ -277,11 +279,20 @@
                                 ExitSuccess  ->  if null errors
                                                  then return $ Right $ map clean (filter (not . null) (lines contents))
                                                  else return $ Left errors
-                                ExitFailure n -> return $ Left $  "Failed to invoke " ++ nm
-                                                               ++ "\nExecutable: " ++ show execPath
-                                                               ++ "\nOptions   : " ++ unwords opts
-                                                               ++ "\nExit code : " ++ show n
+                                ExitFailure n -> let errors' = if null (dropWhile isSpace errors)
+                                                               then "(No error message printed on stderr by the executable.)"
+                                                               else errors
+                                                 in return $ Left $  "Failed to complete the call to " ++ nm
+                                                                  ++ "\nExecutable: " ++ show execPath
+                                                                  ++ "\nOptions   : " ++ unwords opts
+                                                                  ++ "\nExit code : " ++ show n
+                                                                  ++ "\nError message:"
+                                                                  ++ "\n" ++ line ++ "\n"
+                                                                  ++ intercalate "\n" (lines errors')
+                                                                  ++ "\n" ++ line
+                                                                  ++ "\nGiving up.."
   where clean = reverse . dropWhile isSpace . reverse . dropWhile isSpace
+        line  = take 78 $ repeat '='
 
 standardSolver :: SMTConfig -> String -> ([String] -> a) -> ([String] -> a) -> IO a
 standardSolver config script failure success = do
diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs
--- a/Data/SBV/SMT/SMTLib.hs
+++ b/Data/SBV/SMT/SMTLib.hs
@@ -33,8 +33,17 @@
           | Just sw <- s `lookup` aliasTable = (show sw, c)
           | True                             = (s, c)
 
-toSMTLib :: Bool -> [(SW, String)] -> [(SW, CW)] -> [((Int, Int, Int), [SW])] -> [(Int, ArrayInfo)] -> [(String, SBVType)] -> Pgm -> SW -> SMTLibPgm
-toSMTLib isSat inps consts tbls arrs uis asgnsSeq out = SMTLibPgm (aliasTable, pre, post)
+toSMTLib :: Bool                        -- ^ is this a sat problem?
+         -> [(SW, String)]              -- ^ inputs and aliasing names
+         -> [(SW, CW)]                  -- ^ constants
+         -> [((Int, Int, Int), [SW])]   -- ^ auto-generated tables
+         -> [(Int, ArrayInfo)]          -- ^ user specified arrays
+         -> [(String, SBVType)]         -- ^ uninterpreted functions/constants
+         -> [(String, [String])]        -- ^ user given axioms
+         -> Pgm                         -- ^ assignments
+         -> SW                          -- ^ output variable
+         -> SMTLibPgm
+toSMTLib isSat inps consts tbls arrs uis axs asgnsSeq out = SMTLibPgm (aliasTable, pre, post)
   where logic
          | null tbls && null arrs && null uis = "QF_BV"
          | True                               = "QF_AUFBV"
@@ -56,6 +65,8 @@
               ++ concatMap declArray arrs
               ++ [ " ; --- uninterpreted constants ---" ]
               ++ concatMap declUI uis
+              ++ [ " ; --- user given axioms ---" ]
+              ++ map declAx axs
               ++ [ " ; --- assignments ---" ]
               ++ map cvtAsgn asgns
         post =    [ " ; --- formula ---" ]
@@ -83,6 +94,9 @@
                    in [ " :extrafuns ((" ++ iv ++ " BitVec[" ++ show at ++ "]))"
                       , " :assumption (= (select " ++ nm ++ " " ++ iv ++ ") " ++ show sw ++ ")"
                       ]
+
+declAx :: (String, [String]) -> String
+declAx (nm, ls) = (" ;; -- user given axiom: " ++ nm ++ "\n   ") ++ intercalate "\n   " ls
 
 declUI :: (String, SBVType) -> [String]
 declUI (i, t) = [" :extrafuns ((uninterpreted_" ++ i ++ " " ++ cvtType t ++ "))"]
diff --git a/Data/SBV/TestSuite/PrefixSum/PrefixSum.hs b/Data/SBV/TestSuite/PrefixSum/PrefixSum.hs
--- a/Data/SBV/TestSuite/PrefixSum/PrefixSum.hs
+++ b/Data/SBV/TestSuite/PrefixSum/PrefixSum.hs
@@ -18,7 +18,8 @@
 
 -- Test suite
 testSuite :: SBVTestSuite
-testSuite = mkTestSuite $ \_ -> test [
-   "prefixSum1" ~: assert =<< isTheorem (flIsCorrect  8 (0, (+)))
- , "prefixSum1" ~: assert =<< isTheorem (flIsCorrect 16 (0, smax))
- ]
+testSuite = mkTestSuite $ \goldCheck -> test [
+    "prefixSum1" ~: assert =<< isTheorem (flIsCorrect  8 (0, (+)))
+  , "prefixSum2" ~: assert =<< isTheorem (flIsCorrect 16 (0, smax))
+  , "prefixSum3" ~: runSymbolic (genPrefixSumInstance 16) `goldCheck` "prefixSum_16.gold"
+  ]
diff --git a/Data/SBV/TestSuite/Uninterpreted/AUF.hs b/Data/SBV/TestSuite/Uninterpreted/AUF.hs
--- a/Data/SBV/TestSuite/Uninterpreted/AUF.hs
+++ b/Data/SBV/TestSuite/Uninterpreted/AUF.hs
@@ -19,7 +19,8 @@
 -- Test suite
 testSuite :: SBVTestSuite
 testSuite = mkTestSuite $ \goldCheck -> test [
-   "auf-0" ~: assert =<< isTheorem thm
- , "auf-1" ~: pgm `goldCheck` "auf-1.gold"
+   "auf-0" ~: assert =<< isTheorem thm1
+ , "auf-1" ~: assert =<< isTheorem thm2
+ , "auf-2" ~: pgm `goldCheck` "auf-1.gold"
  ]
- where pgm = runSymbolic $ forAll ["x", "y", "a", "initVal"] thm
+ where pgm = runSymbolic $ forAll ["x", "y", "a", "initVal"] thm1
diff --git a/SBVUnitTest/GoldFiles/auf-1.gold b/SBVUnitTest/GoldFiles/auf-1.gold
--- a/SBVUnitTest/GoldFiles/auf-1.gold
+++ b/SBVUnitTest/GoldFiles/auf-1.gold
@@ -12,6 +12,7 @@
 ARRAYS
 UNINTERPRETED CONSTANTS
   uninterpreted_f :: SWord32 -> SWord64
+AXIOMS
 DEFINE
   s4 :: SWord32 = s0 + s3
   s5 :: SBool = s1 == s4
diff --git a/SBVUnitTest/GoldFiles/basic-2_1.gold b/SBVUnitTest/GoldFiles/basic-2_1.gold
--- a/SBVUnitTest/GoldFiles/basic-2_1.gold
+++ b/SBVUnitTest/GoldFiles/basic-2_1.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s1 - s0
diff --git a/SBVUnitTest/GoldFiles/basic-2_2.gold b/SBVUnitTest/GoldFiles/basic-2_2.gold
--- a/SBVUnitTest/GoldFiles/basic-2_2.gold
+++ b/SBVUnitTest/GoldFiles/basic-2_2.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 * s0
   s3 :: SWord8 = s1 - s2
diff --git a/SBVUnitTest/GoldFiles/basic-2_3.gold b/SBVUnitTest/GoldFiles/basic-2_3.gold
--- a/SBVUnitTest/GoldFiles/basic-2_3.gold
+++ b/SBVUnitTest/GoldFiles/basic-2_3.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s2 * s2
diff --git a/SBVUnitTest/GoldFiles/basic-2_4.gold b/SBVUnitTest/GoldFiles/basic-2_4.gold
--- a/SBVUnitTest/GoldFiles/basic-2_4.gold
+++ b/SBVUnitTest/GoldFiles/basic-2_4.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s2 * s2
diff --git a/SBVUnitTest/GoldFiles/basic-3_1.gold b/SBVUnitTest/GoldFiles/basic-3_1.gold
--- a/SBVUnitTest/GoldFiles/basic-3_1.gold
+++ b/SBVUnitTest/GoldFiles/basic-3_1.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s0 - s1
diff --git a/SBVUnitTest/GoldFiles/basic-3_2.gold b/SBVUnitTest/GoldFiles/basic-3_2.gold
--- a/SBVUnitTest/GoldFiles/basic-3_2.gold
+++ b/SBVUnitTest/GoldFiles/basic-3_2.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 * s0
   s3 :: SWord8 = s1 * s1
diff --git a/SBVUnitTest/GoldFiles/basic-3_3.gold b/SBVUnitTest/GoldFiles/basic-3_3.gold
--- a/SBVUnitTest/GoldFiles/basic-3_3.gold
+++ b/SBVUnitTest/GoldFiles/basic-3_3.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s2 * s2
diff --git a/SBVUnitTest/GoldFiles/basic-3_4.gold b/SBVUnitTest/GoldFiles/basic-3_4.gold
--- a/SBVUnitTest/GoldFiles/basic-3_4.gold
+++ b/SBVUnitTest/GoldFiles/basic-3_4.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s2 * s2
diff --git a/SBVUnitTest/GoldFiles/basic-3_5.gold b/SBVUnitTest/GoldFiles/basic-3_5.gold
--- a/SBVUnitTest/GoldFiles/basic-3_5.gold
+++ b/SBVUnitTest/GoldFiles/basic-3_5.gold
@@ -8,6 +8,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s3 :: SWord8 = s0 + s2
 OUTPUTS
diff --git a/SBVUnitTest/GoldFiles/basic-4_1.gold b/SBVUnitTest/GoldFiles/basic-4_1.gold
--- a/SBVUnitTest/GoldFiles/basic-4_1.gold
+++ b/SBVUnitTest/GoldFiles/basic-4_1.gold
@@ -6,6 +6,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s1 :: SWord8 = s0 + s0
   s2 :: SWord8 = s0 - s0
diff --git a/SBVUnitTest/GoldFiles/basic-4_2.gold b/SBVUnitTest/GoldFiles/basic-4_2.gold
--- a/SBVUnitTest/GoldFiles/basic-4_2.gold
+++ b/SBVUnitTest/GoldFiles/basic-4_2.gold
@@ -6,6 +6,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s1 :: SWord8 = s0 * s0
   s2 :: SWord8 = s1 - s1
diff --git a/SBVUnitTest/GoldFiles/basic-4_3.gold b/SBVUnitTest/GoldFiles/basic-4_3.gold
--- a/SBVUnitTest/GoldFiles/basic-4_3.gold
+++ b/SBVUnitTest/GoldFiles/basic-4_3.gold
@@ -6,6 +6,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s1 :: SWord8 = s0 + s0
   s2 :: SWord8 = s1 * s1
diff --git a/SBVUnitTest/GoldFiles/basic-4_4.gold b/SBVUnitTest/GoldFiles/basic-4_4.gold
--- a/SBVUnitTest/GoldFiles/basic-4_4.gold
+++ b/SBVUnitTest/GoldFiles/basic-4_4.gold
@@ -6,6 +6,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s1 :: SWord8 = s0 + s0
   s2 :: SWord8 = s1 * s1
diff --git a/SBVUnitTest/GoldFiles/basic-4_5.gold b/SBVUnitTest/GoldFiles/basic-4_5.gold
--- a/SBVUnitTest/GoldFiles/basic-4_5.gold
+++ b/SBVUnitTest/GoldFiles/basic-4_5.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
 OUTPUTS
diff --git a/SBVUnitTest/GoldFiles/basic-5_1.gold b/SBVUnitTest/GoldFiles/basic-5_1.gold
--- a/SBVUnitTest/GoldFiles/basic-5_1.gold
+++ b/SBVUnitTest/GoldFiles/basic-5_1.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s0
   s3 :: SWord8 = s0 - s0
diff --git a/SBVUnitTest/GoldFiles/basic-5_2.gold b/SBVUnitTest/GoldFiles/basic-5_2.gold
--- a/SBVUnitTest/GoldFiles/basic-5_2.gold
+++ b/SBVUnitTest/GoldFiles/basic-5_2.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 * s0
   s3 :: SWord8 = s2 - s2
diff --git a/SBVUnitTest/GoldFiles/basic-5_3.gold b/SBVUnitTest/GoldFiles/basic-5_3.gold
--- a/SBVUnitTest/GoldFiles/basic-5_3.gold
+++ b/SBVUnitTest/GoldFiles/basic-5_3.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s0
   s3 :: SWord8 = s2 * s2
diff --git a/SBVUnitTest/GoldFiles/basic-5_4.gold b/SBVUnitTest/GoldFiles/basic-5_4.gold
--- a/SBVUnitTest/GoldFiles/basic-5_4.gold
+++ b/SBVUnitTest/GoldFiles/basic-5_4.gold
@@ -7,6 +7,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s0
   s3 :: SWord8 = s2 * s2
diff --git a/SBVUnitTest/GoldFiles/basic-5_5.gold b/SBVUnitTest/GoldFiles/basic-5_5.gold
--- a/SBVUnitTest/GoldFiles/basic-5_5.gold
+++ b/SBVUnitTest/GoldFiles/basic-5_5.gold
@@ -8,6 +8,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s3 :: SWord8 = s0 + s2
 OUTPUTS
diff --git a/SBVUnitTest/GoldFiles/ccitt.gold b/SBVUnitTest/GoldFiles/ccitt.gold
--- a/SBVUnitTest/GoldFiles/ccitt.gold
+++ b/SBVUnitTest/GoldFiles/ccitt.gold
@@ -78,6 +78,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s4 :: SBool = s0 == s2
   s5 :: SBool = s1 == s3
diff --git a/SBVUnitTest/GoldFiles/dogCatMouse.gold b/SBVUnitTest/GoldFiles/dogCatMouse.gold
--- a/SBVUnitTest/GoldFiles/dogCatMouse.gold
+++ b/SBVUnitTest/GoldFiles/dogCatMouse.gold
@@ -1,5 +1,4 @@
-One solution found
-Satisfiable. Model:
+Only one solution found:
   s0 = 3 :: SWord16
   s1 = 41 :: SWord16
   s2 = 56 :: SWord16
diff --git a/SBVUnitTest/GoldFiles/legato.gold b/SBVUnitTest/GoldFiles/legato.gold
--- a/SBVUnitTest/GoldFiles/legato.gold
+++ b/SBVUnitTest/GoldFiles/legato.gold
@@ -19,6 +19,7 @@
 TABLES
 ARRAYS
 UNINTERPRETED CONSTANTS
+AXIOMS
 DEFINE
   s10 :: SBool = s0 /= s2
   s11 :: SBool = s0 /= s4
diff --git a/SBVUnitTest/GoldFiles/prefixSum_16.gold b/SBVUnitTest/GoldFiles/prefixSum_16.gold
new file mode 100644
--- /dev/null
+++ b/SBVUnitTest/GoldFiles/prefixSum_16.gold
@@ -0,0 +1,117 @@
+INPUTS
+  s0 :: SWord32
+  s1 :: SWord32
+  s2 :: SWord32
+  s3 :: SWord32
+  s4 :: SWord32
+  s5 :: SWord32
+  s6 :: SWord32
+  s7 :: SWord32
+  s8 :: SWord32
+  s9 :: SWord32
+  s10 :: SWord32
+  s11 :: SWord32
+  s12 :: SWord32
+  s13 :: SWord32
+  s14 :: SWord32
+  s15 :: SWord32
+CONSTANTS
+  s_2 = False
+  s_1 = True
+TABLES
+ARRAYS
+UNINTERPRETED CONSTANTS
+  uninterpreted_flOp :: SWord32 -> SWord32 -> SWord32
+  uninterpreted_u :: SWord32
+AXIOMS
+  -- user defined axiom: flOp is associative
+  :assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])
+                      (= (uninterpreted_flOp (uninterpreted_flOp ?x ?y) ?z)
+                         (uninterpreted_flOp ?x (uninterpreted_flOp ?y ?z))
+                      )
+              )
+  -- user defined axiom: u is left-unit for flOp
+  :assumption (forall (?x BitVec[32])
+                      (= (uninterpreted_flOp uninterpreted_u ?x)
+                         ?x
+                      )
+              )
+DEFINE
+  s16 :: SWord32 = uninterpreted_u
+  s17 :: SWord32 = s16 uninterpreted_flOp s0
+  s18 :: SBool = s0 == s17
+  s19 :: SWord32 = s0 uninterpreted_flOp s1
+  s20 :: SWord32 = s16 uninterpreted_flOp s19
+  s21 :: SBool = s19 == s20
+  s22 :: SWord32 = s19 uninterpreted_flOp s2
+  s23 :: SWord32 = s20 uninterpreted_flOp s2
+  s24 :: SBool = s22 == s23
+  s25 :: SWord32 = s22 uninterpreted_flOp s3
+  s26 :: SWord32 = s2 uninterpreted_flOp s3
+  s27 :: SWord32 = s19 uninterpreted_flOp s26
+  s28 :: SWord32 = s16 uninterpreted_flOp s27
+  s29 :: SBool = s25 == s28
+  s30 :: SWord32 = s25 uninterpreted_flOp s4
+  s31 :: SWord32 = s28 uninterpreted_flOp s4
+  s32 :: SBool = s30 == s31
+  s33 :: SWord32 = s30 uninterpreted_flOp s5
+  s34 :: SWord32 = s4 uninterpreted_flOp s5
+  s35 :: SWord32 = s28 uninterpreted_flOp s34
+  s36 :: SBool = s33 == s35
+  s37 :: SWord32 = s33 uninterpreted_flOp s6
+  s38 :: SWord32 = s35 uninterpreted_flOp s6
+  s39 :: SBool = s37 == s38
+  s40 :: SWord32 = s37 uninterpreted_flOp s7
+  s41 :: SWord32 = s6 uninterpreted_flOp s7
+  s42 :: SWord32 = s34 uninterpreted_flOp s41
+  s43 :: SWord32 = s27 uninterpreted_flOp s42
+  s44 :: SWord32 = s16 uninterpreted_flOp s43
+  s45 :: SBool = s40 == s44
+  s46 :: SWord32 = s40 uninterpreted_flOp s8
+  s47 :: SWord32 = s44 uninterpreted_flOp s8
+  s48 :: SBool = s46 == s47
+  s49 :: SWord32 = s46 uninterpreted_flOp s9
+  s50 :: SWord32 = s8 uninterpreted_flOp s9
+  s51 :: SWord32 = s44 uninterpreted_flOp s50
+  s52 :: SBool = s49 == s51
+  s53 :: SWord32 = s49 uninterpreted_flOp s10
+  s54 :: SWord32 = s51 uninterpreted_flOp s10
+  s55 :: SBool = s53 == s54
+  s56 :: SWord32 = s53 uninterpreted_flOp s11
+  s57 :: SWord32 = s10 uninterpreted_flOp s11
+  s58 :: SWord32 = s50 uninterpreted_flOp s57
+  s59 :: SWord32 = s44 uninterpreted_flOp s58
+  s60 :: SBool = s56 == s59
+  s61 :: SWord32 = s56 uninterpreted_flOp s12
+  s62 :: SWord32 = s59 uninterpreted_flOp s12
+  s63 :: SBool = s61 == s62
+  s64 :: SWord32 = s61 uninterpreted_flOp s13
+  s65 :: SWord32 = s12 uninterpreted_flOp s13
+  s66 :: SWord32 = s59 uninterpreted_flOp s65
+  s67 :: SBool = s64 == s66
+  s68 :: SWord32 = s64 uninterpreted_flOp s14
+  s69 :: SWord32 = s66 uninterpreted_flOp s14
+  s70 :: SBool = s68 == s69
+  s71 :: SWord32 = s68 uninterpreted_flOp s15
+  s72 :: SWord32 = s14 uninterpreted_flOp s15
+  s73 :: SWord32 = s65 uninterpreted_flOp s72
+  s74 :: SWord32 = s58 uninterpreted_flOp s73
+  s75 :: SWord32 = s43 uninterpreted_flOp s74
+  s76 :: SBool = s71 == s75
+  s77 :: SBool = s70 & s76
+  s78 :: SBool = s67 & s77
+  s79 :: SBool = s63 & s78
+  s80 :: SBool = s60 & s79
+  s81 :: SBool = s55 & s80
+  s82 :: SBool = s52 & s81
+  s83 :: SBool = s48 & s82
+  s84 :: SBool = s45 & s83
+  s85 :: SBool = s39 & s84
+  s86 :: SBool = s36 & s85
+  s87 :: SBool = s32 & s86
+  s88 :: SBool = s29 & s87
+  s89 :: SBool = s24 & s88
+  s90 :: SBool = s21 & s89
+  s91 :: SBool = s18 & s90
+OUTPUTS
+  s91
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,5 +1,5 @@
 Name:          sbv
-Version:       0.9.8
+Version:       0.9.9
 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
 Synopsis:      Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.
 Description:   Express properties about bit-precise Haskell programs and automatically prove