diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -71,6 +71,9 @@
   , geq
   , leq
   , bvULt
+  , bvULeq
+  , bvSLt
+  , bvSLeq
 
     -- ** Arithmetic
   , add
@@ -89,13 +92,18 @@
   , bvNot
   , bvNeg
   , bvAnd
+  , bvXOr
   , bvOr
   , bvAdd
+  , bvSub
   , bvMul
   , bvUDiv
   , bvURem
+  , bvSDiv
+  , bvSRem
   , bvShl
   , bvLShr
+  , bvAShr
 
     -- ** Arrays
   , select
@@ -446,7 +454,9 @@
 --      up so that it is.
 --    * The width should be strictly positive.
 bvHex :: Int {- ^ Width, in bits -} -> Integer {- ^ Value -} -> SExpr
-bvHex w v = const ("#x" ++ padding ++ hex)
+bvHex w v
+  | v >= 0    = const ("#x" ++ padding ++ hex)
+  | otherwise = bvHex w (2^w + v)
   where
   hex     = showHex v ""
   padding = replicate (P.div (w + 3) 4 - length hex) '0'
@@ -522,9 +532,21 @@
 bvULt :: SExpr -> SExpr -> SExpr
 bvULt x y = fun "bvult" [x,y]
 
+-- | Unsigned less-than-or-equal on bit-vectors.
+bvULeq :: SExpr -> SExpr -> SExpr
+bvULeq x y = fun "bvule" [x,y]
 
+-- | Signed less-than on bit-vectors.
+bvSLt :: SExpr -> SExpr -> SExpr
+bvSLt x y = fun "bvslt" [x,y]
 
+-- | Signed less-than-or-equal on bit-vectors.
+bvSLeq :: SExpr -> SExpr -> SExpr
+bvSLeq x y = fun "bvsle" [x,y]
 
+
+
+
 -- | Addition.
 -- See also 'bvAdd'
 add :: SExpr -> SExpr -> SExpr
@@ -583,6 +605,10 @@
 bvOr :: SExpr -> SExpr -> SExpr
 bvOr x y = fun "bvor" [x,y]
 
+-- | Bitwsie exclusive or.
+bvXOr :: SExpr -> SExpr -> SExpr
+bvXOr x y = fun "bvxor" [x,y]
+
 -- | Bit vector arithmetic negation.
 bvNeg :: SExpr -> SExpr
 bvNeg x = fun "bvneg" [x]
@@ -591,6 +617,12 @@
 bvAdd :: SExpr -> SExpr -> SExpr
 bvAdd x y = fun "bvadd" [x,y]
 
+-- | Subtraction of bit vectors.
+bvSub :: SExpr -> SExpr -> SExpr
+bvSub x y = fun "bvsub" [x,y]
+
+
+
 -- | Multiplication of bit vectors.
 bvMul :: SExpr -> SExpr -> SExpr
 bvMul x y = fun "bvmul" [x,y]
@@ -603,6 +635,17 @@
 bvURem :: SExpr -> SExpr -> SExpr
 bvURem x y = fun "bvurem" [x,y]
 
+-- | Bit vector signed division.
+bvSDiv :: SExpr -> SExpr -> SExpr
+bvSDiv x y = fun "bvsdiv" [x,y]
+
+-- | Bit vector signed reminder.
+bvSRem :: SExpr -> SExpr -> SExpr
+bvSRem x y = fun "bvsrem" [x,y]
+
+
+
+
 -- | Shift left.
 bvShl :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
 bvShl x y = fun "bvshl" [x,y]
@@ -610,6 +653,10 @@
 -- | Logical shift right.
 bvLShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
 bvLShr x y = fun "bvshr" [x,y]
+
+-- | Arithemti shift right (copies most significant bit).
+bvAShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr
+bvAShr x y = fun "bvashr" [x,y]
 
 -- | Get an elemeent of an array.
 select :: SExpr {- ^ array -} -> SExpr {- ^ index -} -> 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.4.0
+version:             0.5.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