diff --git a/boolector.cabal b/boolector.cabal
--- a/boolector.cabal
+++ b/boolector.cabal
@@ -1,5 +1,5 @@
 name:                boolector
-version:             0.0.0.7
+version:             0.0.0.8
 synopsis:            Haskell bindings for the Boolector SMT solver
 description:
 
@@ -35,7 +35,8 @@
         containers,
         mtl,
         temporary,
-        directory
+        directory,
+        time
 
   ghc-options: -Wall -fno-warn-orphans
   build-tools:      c2hs
@@ -113,5 +114,14 @@
                , boolector
   Type: exitcode-stdio-1.0
   main-is: UF_Example2.hs
+  extra-libraries:  boolector
+  hs-source-dirs: test
+
+Test-Suite Const_Example
+  default-language: Haskell2010
+  Build-Depends: base >= 4.7 && < 5
+               , boolector
+  Type: exitcode-stdio-1.0
+  main-is: Const_Example.hs
   extra-libraries:  boolector
   hs-source-dirs: test
diff --git a/src/Boolector.hs b/src/Boolector.hs
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -209,6 +209,10 @@
                  , unsignedBvAssignment
                  , signedBvAssignment
                  , boolAssignment
+                 -- ** Constant nodes
+                 , boolConst
+                 , signedBvConst
+                 , unsignedBvConst
                  -- ** Sorts
                  , Sort
                  , SortTy, sortTy
@@ -245,8 +249,11 @@
 import Control.Applicative ((<$>))
 import Control.Monad.State.Strict
 import Control.Exception hiding (assert)
-import Control.Concurrent
 
+import Data.Time.Clock
+import Data.Time.Clock.TAI
+import Data.Time.Clock.System
+
 import Prelude hiding (read, not, and, or, const, concat, repeat)
 import qualified Prelude as Prelude
 
@@ -284,7 +291,7 @@
 
 -- | Create new Boolector state with optional timeout. By default, we enable
 -- support for model generation and incremental solving.
-newBoolectorState :: Maybe Int -> IO BoolectorState
+newBoolectorState :: Maybe Integer -> IO BoolectorState
 newBoolectorState Nothing = do
   b <- B.new
   B.setOpt b OPT_MODEL_GEN 2
@@ -292,12 +299,12 @@
   B.setOpt b OPT_INCREMENTAL 1
   return $ BoolectorState b emptyBoolectorCache
 newBoolectorState (Just time) = do
-  term <- newMVar 0
   btorState@(BoolectorState b _) <- newBoolectorState Nothing
+  t0 <- systemToTAITime `liftM` getSystemTime
   B.setTerm b $ \_ -> do
-    readMVar term
-  void $ forkIO $ do threadDelay $ time * 1000
-                     putMVar term 1 -- this will cause boolector eval to fail if not done
+    t1 <- systemToTAITime `liftM` getSystemTime
+    let shouldTerminate = diffAbsoluteTime t1 t0 > secondsToDiffTime time
+    return $ if shouldTerminate then 1 else 0
   return btorState
 
 -- | Set option.
@@ -406,7 +413,7 @@
 
 -- | Create bit vector constant of sort @sort@, where each bit is set to one.
 ones :: MonadBoolector m => Sort -> m Node
-ones srt = mkNode onesStr $ liftBoolector1 B.one $ _sort srt
+ones srt = mkNode onesStr $ liftBoolector1 B.ones $ _sort srt
   where onesStr = "0b" ++ replicate nr '1'
         nr = case sortTy srt of
               BoolSort -> 1
@@ -887,6 +894,10 @@
 setSymbol :: MonadBoolector m => Node -> String -> m ()
 setSymbol n str = liftBoolector2 B.setSymbol (_node n) str
 
+-- | Get the bit vector of a constant node as a bit string.
+getBits :: MonadBoolector m => Node -> m String
+getBits = liftBoolector1 B.getBits . _node
+
 -- | Get the bit width of an expression.
 --
 -- If the expression is an array, it returns the bit width of the array
@@ -937,6 +948,51 @@
 -- Models.
 --
 
+-- | Get the bool value of a constant node if it is constant.
+boolConst :: MonadBoolector m => Node -> m (Maybe Bool)
+boolConst node = do
+  cnst <- isConst node
+  if cnst
+    then do str <- getBits node
+            Just `liftM` bitsToBool str
+    else return Nothing
+
+-- | Get the unsigned integer value of a constant node if it is constant.
+unsignedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
+unsignedBvConst node = do
+  cnst <- isConst node
+  if cnst
+    then do str <- getBits node
+            Just `liftM` bitsToUnsignedInteger str
+    else return Nothing
+
+-- | Get the signed integer value of a constant node if it is constant.
+signedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
+signedBvConst node = do
+  cnst <- isConst node
+  if cnst
+    then do str <- getBits node
+            val <- bitsToUnsignedInteger str
+            w <- getWidth node
+            let max_signed_w = 2 ^ pred w
+            return . Just $ if val >= max_signed_w
+                              then val - (2*max_signed_w)
+                              else val
+    else return Nothing
+
+-- | Helper for converting bit-string to an unsigned integer.
+bitsToUnsignedInteger :: MonadBoolector m => String -> m Integer
+bitsToUnsignedInteger str = do
+  when (Prelude.not $ all isDigit str) $ error $ "getModelVal: not numeric: " ++ str
+  liftIO $ evaluate $ foldl (\ n c -> 2 * n + Prelude.read [c]) 0 str
+
+-- | Helper for converting bit-string to a boolean.
+bitsToBool :: MonadBoolector m => String -> m Bool
+bitsToBool str = liftIO $ evaluate $ case str of
+  "0" -> False
+  "1" -> True
+  _   -> error $ "bitsToBool: not boolean: " ++ str
+
 -- | Generate an assignment string for bit vector expression if
 -- boolector_sat has returned BOOLECTOR_SAT and model generation has been
 -- enabled.
@@ -951,8 +1007,7 @@
 unsignedBvAssignment :: MonadBoolector m => Node -> m Integer
 unsignedBvAssignment node = do
   str <- bvAssignment node
-  when (Prelude.not $ all isDigit str) $ error $ "getModelVal: not numeric: " ++ str
-  liftIO $ evaluate $ foldl (\ n c -> 2 * n + Prelude.read [c]) 0 str
+  bitsToUnsignedInteger str
 
 -- | Get signed integer value from model.
 signedBvAssignment :: MonadBoolector m => Node -> m Integer
@@ -968,10 +1023,7 @@
 boolAssignment :: MonadBoolector m => Node -> m Bool
 boolAssignment node = do
     str <- bvAssignment node
-    liftIO $ evaluate $ case str of
-        "0" -> False
-        "1" -> True
-        _   -> error $ "boolAssignment: not boolean: " ++ str
+    bitsToBool str
 
 --
 -- Sorts
diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs
--- a/src/Boolector/Foreign.chs
+++ b/src/Boolector/Foreign.chs
@@ -122,6 +122,7 @@
   , getFunArity
   , getSymbol
   , setSymbol
+  , getBits
   , getWidth
   , getIndexWidth
   , isConst
@@ -787,6 +788,10 @@
 
 -- | Set the symbol of an expression.
 {#fun set_symbol as ^ { `Btor' , `Node', `String' } -> `()' #}
+
+-- | Get the bit vector of a constant node as a bit string.
+{#fun get_bits as ^ { `Btor' , `Node' } -> `String' #}
+
 
 -- | Get the bit width of an expression.
 --
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
@@ -6,8 +6,8 @@
 
 main :: IO ()
 main = do
-  -- Create new Boolector state with a 1000ms timeout
-  bs <- B.newBoolectorState (Just 1000)
+  -- Create new Boolector state with a 1s timeout
+  bs <- B.newBoolectorState (Just 1)
   B.evalBoolector bs $ do
     -- Create a 8-bit bit-vector
     u8 <- B.bitvecSort 8
diff --git a/test/Const_Example.hs b/test/Const_Example.hs
new file mode 100644
--- /dev/null
+++ b/test/Const_Example.hs
@@ -0,0 +1,24 @@
+import qualified Boolector as B
+
+import Control.Monad.IO.Class
+import Control.Exception (assert)
+import Control.Concurrent
+
+main :: IO ()
+main = do
+  -- Create new Boolector state with a 1s timeout
+  bs <- B.newBoolectorState (Just 1)
+  B.evalBoolector bs $ do
+    -- Create a 8-bit bit-vector
+    u8 <- B.bitvecSort 8
+
+    -- Create a constant value and two variables of sort u8
+    c <- B.unsignedInt 35 u8
+    x <- B.var u8 "x"
+
+    -- Get model
+    mc <- B.signedBvConst c
+    mx <- B.signedBvConst x
+    assert (mc == Just 35) $ return ()
+    assert (mx == Nothing) $ return ()
+
diff --git a/test/GetSetSymbol_Example.hs b/test/GetSetSymbol_Example.hs
--- a/test/GetSetSymbol_Example.hs
+++ b/test/GetSetSymbol_Example.hs
@@ -10,8 +10,8 @@
 
 main :: IO ()
 main = do
-  -- Create new Boolector state with a 1000ms timeout
-  bs <- B.newBoolectorState (Just 1000)
+  -- Create new Boolector state with a 1s timeout
+  bs <- B.newBoolectorState (Just 1)
   B.evalBoolector bs $ do
     -- Create a 8-bit bit-vector
     u8 <- B.bitvecSort 8