diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -22,6 +22,7 @@
 
     -- * Common SmtLib-2 Commands
   , setLogic
+  , setOption
   , push, pushMany
   , pop, popMany
   , declare
@@ -51,6 +52,7 @@
   , bool
   , bvBin
   , bvHex
+  , value
 
     -- ** Connectives
   , not
@@ -264,7 +266,7 @@
 
 -- | Pop multiple scopes.
 popMany :: Solver -> Integer -> IO ()
-popMany proc n = simpleCommand proc [ "push", show n ]
+popMany proc n = simpleCommand proc [ "pop", show n ]
 
 
 
@@ -450,6 +452,17 @@
   padding = replicate (P.div (w + 3) 4 - length hex) '0'
 
 
+-- | Render a value as an expression.  Bit-vectors are rendered in hex,
+-- if their width is a multiple of 4, and in binary otherwise.
+value :: Value -> SExpr
+value val =
+  case val of
+    Bool b    -> bool b
+    Int n     -> int n
+    Real r    -> real r
+    Bits w v | P.mod w 4 == 0 -> bvHex w v
+             | otherwise      -> bvBin w v
+    Other o   -> o
 
 -- Connectives -----------------------------------------------------------------
 
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.2.0.0
+version:             0.3.0
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3