diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,4 @@
+0.9:   Support for working with unsat-cores
 0.8:   Support for declare; loading of strings/files; more sugar for SMT commands
 0.6.0: Allow finer-grained logging
 0.5.5: Add support for unsupported results
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -26,6 +26,8 @@
     -- * Common SmtLib-2 Commands
   , setLogic, setLogicMaybe
   , setOption, setOptionMaybe
+  , produceUnsatCores
+  , named
   , push, pushMany
   , pop, popMany
   , inNewScope
@@ -39,7 +41,9 @@
   , Result(..)
   , getExprs, getExpr
   , getConsts, getConst
+  , getUnsatCore
   , Value(..)
+  , sexprToVal
 
     -- * Convenience Functions for SmtLib-2 Epxressions
   , fam
@@ -322,10 +326,14 @@
 setLogic :: Solver -> String -> IO ()
 setLogic s x = simpleCommand s [ "set-logic", x ]
 
+
 -- | Set the solver's logic, returning False if the logic is unsupported.
 setLogicMaybe :: Solver -> String -> IO Bool
 setLogicMaybe s x = simpleCommandMaybe s [ "set-logic", x ]
 
+-- | Request unsat cores.  Returns if the solver supports them.
+produceUnsatCores :: Solver -> IO Bool
+produceUnsatCores s = setOptionMaybe s ":produce-unsat-cores" "true"
 
 -- | Checkpoint state.  A special case of 'pushMany'.
 push :: Solver -> IO ()
@@ -497,7 +505,25 @@
 getConst :: Solver -> String -> IO Value
 getConst proc x = getExpr proc (Atom x)
 
+-- | Returns the names of the (named) formulas involved in a contradiction.
+getUnsatCore :: Solver -> IO [String]
+getUnsatCore s =
+  do res <- command s $ List [ Atom "get-unsat-core" ]
+     case res of
+       List xs -> mapM fromAtom xs
+       _       -> unexpected "a list of atoms" res
+  where
+  fromAtom x =
+    case x of
+      Atom a -> return a
+      _      -> unexpected "an atom" x
 
+  unexpected x e =
+    fail $ unlines [ "Unexpected response from the SMT Solver:"
+                   , "  Expected: " ++ x
+                   , "  Result: " ++ showsSExpr e ""
+                   ]
+
 --------------------------------------------------------------------------------
 
 
@@ -812,6 +838,12 @@
          SExpr
 store x y z = fun "store" [x,y,z]
 
+
+--------------------------------------------------------------------------------
+-- Attributes
+
+named :: String -> SExpr -> SExpr
+named x e = fun "!" [e, Atom ":named", Atom x ]
 
 
 --------------------------------------------------------------------------------
diff --git a/simple-smt.cabal b/simple-smt.cabal
--- a/simple-smt.cabal
+++ b/simple-smt.cabal
@@ -1,5 +1,5 @@
 name:                simple-smt
-version:             0.8
+version:             0.9.1
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3