diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,5 @@
+0.9.3: Fix incorrect rendering or `real` literals
+0.9.2: add ppSExpr
 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
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -14,7 +14,7 @@
 
     -- ** S-Expressions
   , SExpr(..)
-  , showsSExpr, readSExpr
+  , showsSExpr, ppSExpr, readSExpr
 
     -- ** Logging and Debugging
   , Logger(..)
@@ -130,7 +130,7 @@
 import Prelude hiding (not, and, or, abs, div, mod, concat, const)
 import qualified Prelude as P
 import Data.Char(isSpace)
-import Data.List(unfoldr)
+import Data.List(unfoldr,intersperse)
 import Data.Bits(testBit)
 import Data.IORef(newIORef, atomicModifyIORef, modifyIORef', readIORef,
                   writeIORef)
@@ -142,7 +142,7 @@
 import Control.Monad(forever,when)
 import Text.Read(readMaybe)
 import Data.Ratio((%), numerator, denominator)
-import Numeric(showHex, readHex)
+import Numeric(showHex, readHex, showFFloat)
 
 
 -- | Results of checking for satisfiability.
@@ -173,6 +173,38 @@
                 foldr (\e m -> showsSExpr e . showChar ' ' . m)
                 (showChar ')') es
 
+
+-- | Show an S-expression in a somewhat readbale fashion.
+ppSExpr :: SExpr -> ShowS
+ppSExpr = go 0
+  where
+  tab n = showString (replicate n ' ')
+  many  = foldr (.) id
+
+  new n e = showChar '\n' . tab n . go n e
+
+  small n es =
+    case es of
+      [] -> Just []
+      e : more
+        | n <= 0 -> Nothing
+        | otherwise -> case e of
+                         Atom x -> (showString x :) <$> small (n-1) more
+                         _      -> Nothing
+
+  go :: Int -> SExpr -> ShowS
+  go n ex =
+    case ex of
+      Atom x        -> showString x
+      List es
+        | Just fs <- small 5 es ->
+          showChar '(' . many (intersperse (showChar ' ') fs) . showChar ')'
+
+      List (Atom x : es) -> showString "(" . showString x .
+                                many (map (new (n+3)) es) . showString ")"
+
+      List es -> showString "(" . many (map (new (n+2)) es) . showString ")"
+
 -- | Parse an s-expression.
 readSExpr :: String -> Maybe (SExpr, String)
 readSExpr (c : more) | isSpace c = readSExpr more
@@ -578,11 +610,14 @@
 -- | Integer literals.
 int :: Integer -> SExpr
 int x | x < 0     = neg (int (negate x))
-         | otherwise = Atom (show x)
+      | otherwise = Atom (show x)
 
 -- | Real (well, rational) literals.
 real :: Rational -> SExpr
-real x = realDiv (int (denominator x)) (int (numerator x))
+real x
+  | toRational y == x = Atom (showFFloat Nothing y "")
+  | otherwise = realDiv (int (numerator x)) (int (denominator x))
+  where y = fromRational x :: Double
 
 -- | A bit vector represented in binary.
 --
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.9.1
+version:             0.9.3
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3