diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,4 @@
+0.9.4: Add `toInt` and `toReal`
 0.9.3: Fix incorrect rendering or `real` literals
 0.9.2: add ppSExpr
 0.9:   Support for working with unsat-cores
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -100,6 +100,8 @@
   , mod
   , divisible
   , realDiv
+  , toInt
+  , toReal
 
     -- ** Bit Vectors
   , concat
@@ -791,6 +793,14 @@
 -- by @i@ bits
 zeroExtend :: Integer -> SExpr -> SExpr
 zeroExtend i x = List [ fam "zero_extend" [i], x ]
+
+-- | Satisfies @toInt x <= x@ (i.e., this is like Haskell's 'floor')
+toInt :: SExpr -> SExpr
+toInt e = fun "to_int" [e]
+
+-- | Promote an integer to a real
+toReal :: SExpr -> SExpr
+toReal e = fun "to_real" [e]
 
 -- | Extract a sub-sequence of a bit vector.
 extract :: SExpr -> Integer -> Integer -> SExpr
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.3
+version:             0.9.4
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3