diff --git a/boolector.cabal b/boolector.cabal
--- a/boolector.cabal
+++ b/boolector.cabal
@@ -1,5 +1,5 @@
 name:                boolector
-version:             0.0.0.2
+version:             0.0.0.3
 synopsis:            Haskell bindings for the Boolector SMT solver
 description:
 
@@ -33,7 +33,9 @@
   build-depends:
         base >= 4.7 && < 5,
         containers,
-        mtl
+        mtl,
+        temporary,
+        directory
 
   ghc-options: -Wall -fno-warn-orphans
   build-tools:      c2hs
diff --git a/src/Boolector.hs b/src/Boolector.hs
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -219,10 +219,11 @@
                  , isFunSort
                  , funSortCheck
                  -- * Debug dumping
-                 , dumpBtorNode
-                 , dumpSmt2Node
-                 , dumpBtor
-                 , dumpSmt2
+                 , dump
+                 , dumpNode
+                 , dumpToString
+                 , dumpNodeToString
+                 , DumpFormat(..)
                  ) where
 
 import Boolector.Foreign (Option(..), Status(..), Node, Sort)
@@ -975,29 +976,47 @@
 -- Dumping
 --
 
--- | Recursively dump @node@ to file in BTOR_ format.
-dumpBtorNode :: MonadBoolector m => FilePath -> Node -> m ()
-dumpBtorNode path node = do
-  file <- liftIO $ B.fopen path "w"
-  liftBoolector2 B.dumpBtorNode file node
+-- | Output dump format.
+data DumpFormat = DumpBtor | DumpSMT2
+      deriving (Eq, Show)
 
--- | Recursively dump @node@ to file in SMT-LIB v2 format.
-dumpSmt2Node :: MonadBoolector m => FilePath -> Node -> m ()
-dumpSmt2Node path node = do
-  file <- liftIO $ B.fopen path "w"
-  liftBoolector2 B.dumpSmt2Node file node
+-- | Recursively dump @node@ to file in BTOR or SMT-LIB v2 format.
+dumpNode :: MonadBoolector m => DumpFormat -> FilePath -> Node -> m ()
+dumpNode fmt path node = do
+  btor <- unBoolectorState `liftM` getBoolectorState
+  liftIO $ B.withDumpFile path $ \file -> dumper btor file node
+  where dumper = case fmt of
+                  DumpBtor -> B.dumpBtorNode
+                  _        -> B.dumpSmt2Node
 
--- | Dump formula to file in BTOR_ format.
-dumpBtor :: MonadBoolector m => FilePath -> m ()
-dumpBtor path = do
-  file <- liftIO $ B.fopen path "w"
-  liftBoolector1 B.dumpBtor file
+-- | Dump formula to file in BTOR or SMT-LIB v2 format.
+dump :: MonadBoolector m => DumpFormat -> FilePath -> m ()
+dump fmt path = do
+  btor <- unBoolectorState `liftM` getBoolectorState
+  liftIO $ B.withDumpFile path (dumper btor)
+  where dumper = case fmt of
+                  DumpBtor -> B.dumpBtor
+                  _        -> B.dumpSmt2
 
--- | Dumps formula to file in SMT-LIB v2 format.
-dumpSmt2 :: MonadBoolector m => FilePath -> m ()
-dumpSmt2 path = do
-  file <- liftIO $ B.fopen path "w"
-  liftBoolector1 B.dumpSmt2 file
+-- | Same as 'dumpNode', but returns string.
+-- TODO: this is super slow, we should request feature from boolector.
+dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String
+dumpNodeToString fmt node = do
+  btor <- unBoolectorState `liftM` getBoolectorState
+  liftIO $ B.withTempDumpFile (\file -> dumper btor file node)
+  where dumper = case fmt of
+                  DumpBtor -> B.dumpBtorNode
+                  _        -> B.dumpSmt2Node
+
+-- | Same as 'dump', but returns string.
+-- TODO: this is super slow, we should request feature from boolector.
+dumpToString :: MonadBoolector m => DumpFormat -> m String
+dumpToString fmt = do
+  btor <- unBoolectorState `liftM` getBoolectorState
+  liftIO $ B.withTempDumpFile (dumper btor)
+  where dumper = case fmt of
+                  DumpBtor -> B.dumpBtor
+                  _        -> B.dumpSmt2
 
 --
 -- Helpers
diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs
--- a/src/Boolector/Foreign.chs
+++ b/src/Boolector/Foreign.chs
@@ -152,7 +152,7 @@
   , dumpBtor
   , dumpSmt2
   -- * Helpers
-  , fopen
+  , withDumpFile, withTempDumpFile 
   , setTerm
   ) where
 
@@ -162,6 +162,9 @@
 import Foreign.C
 
 import Control.Monad
+import Control.Exception (bracket, finally, onException)
+import System.IO.Temp
+import System.Directory (removeFile)
 
 {#context lib = "boolector" prefix = "boolector_" #}
 
@@ -900,10 +903,31 @@
 --
 
 -- | POSIX files
-{#pointer *FILE as File foreign finalizer fclose newtype#}
+{#pointer *FILE as File foreign newtype#}
 
--- | Expose POSIX file open.
+-- | POSIX fopen.
 {#fun fopen as ^ {`String', `String'} -> `File' #}
+
+-- | POSIX fclose.
+{#fun fclose as ^ {`File'} -> `()' #}
+
+-- | POSIX fflush.
+{#fun fflush as ^ {`File'} -> `()' #}
+
+-- | Helper for writing to dump file.
+withDumpFile :: String
+             -> (File -> IO ())
+             -> IO ()
+withDumpFile path act = bracket
+  (fopen path "w") fclose
+  (\fileHandle -> act fileHandle >> fflush fileHandle)
+
+-- | Helper for writing to dump file.
+withTempDumpFile :: (File -> IO ()) -> IO String
+withTempDumpFile act = do
+  path <- emptySystemTempFile "haskell-boolector"
+  withDumpFile path act `onException` removeFile path
+  readFile path `finally` removeFile path
 
 -- | Recursively dump @node@ to file in BTOR_ format.
 {#fun dump_btor_node as ^ { `Btor' , `File', `Node' } -> `()' #}
diff --git a/test/API_Usage_Example.hs b/test/API_Usage_Example.hs
--- a/test/API_Usage_Example.hs
+++ b/test/API_Usage_Example.hs
@@ -30,7 +30,7 @@
     B.assert =<< B.ugt y one
 
     -- Dump the corresponding SMT Lib 2 to a file
-    B.dumpSmt2 "dump_example.smt2"
+    B.dump B.DumpSMT2 "dump_example.smt2"
 
     -- Check satisfiability
     B.Sat <- B.sat
diff --git a/test/Arith_Example.hs b/test/Arith_Example.hs
--- a/test/Arith_Example.hs
+++ b/test/Arith_Example.hs
@@ -32,6 +32,8 @@
     -- (assert (>= (* 2 x) (+ y z)))
     do tmp1 <- B.mul two x
        tmp2 <- B.add y z
+       tmp2Str <- B.dumpNodeToString B.DumpSMT2 tmp2
+       liftIO $ putStrLn $ "tmp2Str = " ++ tmp2Str
        B.assert =<< B.sgte tmp1 tmp2
 
     -- (assert (< (f x) (g x x)))
diff --git a/test/Array_Example.hs b/test/Array_Example.hs
--- a/test/Array_Example.hs
+++ b/test/Array_Example.hs
@@ -24,7 +24,7 @@
     y' <- B.read arr x
     w <- B.var u8 "w"
 
-    B.dumpSmt2 "dump_example.smt2"
+    B.dump B.DumpSMT2 "dump_example.smt2"
     B.sat
     mx  <- B.unsignedBvAssignment x
     my <- B.unsignedBvAssignment y
diff --git a/test/GetSetSymbol_Example.hs b/test/GetSetSymbol_Example.hs
--- a/test/GetSetSymbol_Example.hs
+++ b/test/GetSetSymbol_Example.hs
@@ -41,8 +41,8 @@
     B.assert =<< B.ugt x one
     B.assert =<< B.ugt y one
 
-    -- Dump the corresponding SMT Lib 2 to a file
-    B.dumpSmt2 "dump_example.smt2"
+    -- Dump the corresponding SMT Lib 2
+    B.dumpToString B.DumpSMT2 >>= liftIO . putStrLn
 
     -- Check satisfiability
     B.Sat <- B.sat