diff --git a/Satchmo/Binary.hs b/Satchmo/Binary.hs
--- a/Satchmo/Binary.hs
+++ b/Satchmo/Binary.hs
@@ -2,127 +2,9 @@
 
 module Satchmo.Binary 
 
-( Number, width, number, fixed
-, add, times
-, equals
+( module Satchmo.Binary.Op.Flexible
 )
 
 where
 
-import Prelude hiding ( and, or, not )
-
-import qualified Satchmo.Code as C
-import Satchmo.Boolean
-import Satchmo.Counting
-
-type Booleans = [ Boolean ]
-
-data Number = Number 
-            { encode :: Booleans -- lsb first
-            , decode :: C.Decoder Integer
-            }
-
-instance C.Decode Number Integer where
-    decode = decode
-
-width :: Number -> Int
-width n = length $ encode n
-
--- | declare a number variable (bit width)
-number :: Int -> SAT Number
-number w = do
-    xs <- sequence $ replicate w boolean
-    return $ make xs
-
-make :: [ Boolean ] -> Number
-make xs = Number
-           { encode = xs
-           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys
-           }
-
-fromBinary :: [ Bool ] -> Integer
-fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs
-
-toBinary :: Int -> Integer -> [ Bool ]
-toBinary 0 0 = []
-toBinary b n | b > 0 = 
-    let (d,m) = divMod n 2
-    in  toEnum ( fromIntegral m ) : toBinary (b-1) d
-
--- | declare a number constant (bit width, value)
-fixed :: Int -> Integer -> SAT Number
-fixed b n = do
-    xs <- mapM constant $ toBinary b n
-    return $ make xs
-
--- | result width is 1 + largest argument width
-add :: Number -> Number -> SAT Number
-add ( Number { encode = xs } ) ( Number { encode = ys } ) = do
-    false <- constant False
-    ( zs, carry ) <- add_with_carry false xs ys
-    return $ make $ zs ++ [carry]
-
--- | result width is largest argument width
--- if overflow, then unsatisfiable
-restricted_add :: Number -> Number -> SAT Number 
-restricted_add a b = do
-    c <- add a b
-    restricted ( max (width a) (width b)) c
-
--- | give only lower k bits, upper bits must be zero,
--- (else unsatisfiable)
-restricted :: Int -> Number -> SAT Number
-restricted w ( Number { encode = xs } ) = do
-    let ( low, high ) = splitAt w xs
-    sequence $ do x <- high ; return $ assert [ not x ]
-    return $ make low
-
--- | result has max length of both inputs
-add_with_carry :: Boolean 
-               -> Booleans -> Booleans
-               -> SAT ( Booleans, Boolean )
-add_with_carry cin [] [] = return ( [], cin )
-add_with_carry cin (x:xs) [] = do
-    z <- xor [ cin, x ]
-    c <- and [ cin, x ]
-    ( zs, cout ) <- add_with_carry c xs []
-    return ( z : zs, cout )
-add_with_carry cin [] (y:ys) = do
-    add_with_carry cin (y:ys) []
-add_with_carry cin (x:xs ) (y:ys) = do
-    z  <- xor [ cin, x, y ]
-    c <- atleast 2 [ cin, x, y ]
-    ( zs, cout ) <- add_with_carry c xs ys
-    return ( z : zs, cout )
-
-times :: Number -> Number -> SAT Number
-times ( Number { encode = [x] } ) ys = times1 x ys
-times ( Number { encode = x:xs } ) ys = do
-    xys  <- times1 x ys
-    xsys <- times (make xs) ys
-    zs <- shift xsys
-    add xys zs
-
--- | multiply by 2
-shift :: Number -> SAT Number
-shift ( Number { encode = xs } ) = do
-    false <- constant False 
-    return $ make $ false : xs
-
-times1 :: Boolean -> Number -> SAT Number
-times1 x ( Number { encode = ys } ) = do
-    zs <- mapM ( \ y -> and [x,y] ) ys
-    return $ make zs
-
-equals :: Number -> Number -> SAT Boolean
-equals ( Number { encode = xs } ) ( Number { encode = ys } ) = do
-    equals' xs ys
-
-equals' :: Booleans -> Booleans -> SAT Boolean
-equals' [] [] = constant True
-equals' (x:xs) (y:ys) = do
-    z <- xor [x, y]
-    rest <- equals' xs ys
-    and [ not z, rest ]
-equals' xs [] = and $ map not xs
-equals' [] ys = and $ map not ys
+import Satchmo.Binary.Op.Flexible
diff --git a/Satchmo/Binary/Data.hs b/Satchmo/Binary/Data.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Binary/Data.hs
@@ -0,0 +1,74 @@
+{-# language MultiParamTypeClasses #-}
+
+module Satchmo.Binary.Data
+
+( Number, bits, make
+, width, number, constant
+, equals, iszero
+)
+
+where
+
+import Prelude hiding ( and, or, not )
+
+import qualified Satchmo.Code as C
+
+import Satchmo.Boolean hiding ( constant )
+import qualified  Satchmo.Boolean as B
+
+import Satchmo.Counting
+
+data Number = Number 
+            { bits :: [ Boolean ] -- lsb first
+            , decode :: C.Decoder Integer
+            }
+
+instance C.Decode Number Integer where
+    decode = decode
+
+width :: Number -> Int
+width n = length $ bits n
+
+-- | declare a number variable (bit width)
+number :: Int -> SAT Number
+number w = do
+    xs <- sequence $ replicate w boolean
+    return $ make xs
+
+make :: [ Boolean ] -> Number
+make xs = Number
+           { bits = xs
+           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys
+           }
+
+fromBinary :: [ Bool ] -> Integer
+fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs
+
+toBinary :: Integer -> [ Bool ]
+toBinary 0 = []
+toBinary n  = 
+    let (d,m) = divMod n 2
+    in  toEnum ( fromIntegral m ) : toBinary d
+
+-- | declare a number constant 
+constant :: Integer -> SAT Number
+constant n = do
+    xs <- mapM B.constant $ toBinary n
+    return $ make xs
+
+iszero :: Number -> SAT Boolean
+iszero a = equals a $ make []
+
+equals :: Number -> Number -> SAT Boolean
+equals a b = do
+    equals' ( bits a ) ( bits b )
+
+equals' :: Booleans -> Booleans -> SAT Boolean
+equals' [] [] = B.constant True
+equals' (x:xs) (y:ys) = do
+    z <- xor [x, y]
+    rest <- equals' xs ys
+    and [ not z, rest ]
+equals' xs [] = and $ map not xs
+equals' [] ys = and $ map not ys
+
diff --git a/Satchmo/Binary/Op/Fixed.hs b/Satchmo/Binary/Op/Fixed.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Binary/Op/Fixed.hs
@@ -0,0 +1,90 @@
+{-# language MultiParamTypeClasses #-}
+
+-- | operations with fixed bit width.
+-- still they are non-overflowing:
+-- if overflow occurs, the constraints are not satisfiable.
+-- the bit width of the result of binary operations
+-- is the max of the bit width of the inputs.
+
+module Satchmo.Binary.Op.Fixed
+
+( restricted
+, add, times
+, module Satchmo.Binary.Data
+)
+
+where
+
+import Prelude hiding ( and, or, not )
+
+import qualified Satchmo.Code as C
+
+import Satchmo.Boolean
+import Satchmo.Binary.Data
+import qualified Satchmo.Binary.Op.Flexible as Flexible
+
+import Satchmo.Counting
+
+-- | give only lower k bits, upper bits must be zero,
+-- (else unsatisfiable)
+restricted :: Int -> Number -> SAT Number
+restricted w a = do
+    let ( low, high ) = splitAt w $ bits a
+    sequence $ do x <- high ; return $ assert [ not x ]
+    return $ make low
+
+-- | result bit width is max of argument bit widths.
+-- if overflow occurs, then formula is unsatisfiable.
+add :: Number -> Number -> SAT Number
+add a b = do
+    false <- Satchmo.Boolean.constant False
+    let w = max ( width a ) ( width b )
+    zs <- add_with_carry w false ( bits a ) ( bits b )
+    return $ make zs 
+
+add_with_carry :: Int -> Boolean -> Booleans -> Booleans -> SAT Booleans
+add_with_carry w c xxs yys = case ( xxs, yys ) of
+    _ | w <= 0 -> do
+        sequence_ $ do p <- c : xxs ++ yys ; return $ assert [ not p ]
+        return []
+    ( [] , [] ) -> return [ c ]
+    ( [], y : ys) -> do
+        r <- xor [ c, y ]
+        d <- and [ c, y ]
+        rest <- add_with_carry (w-1) d [] ys
+        return $ r : rest
+    ( x : xs, [] ) -> add_with_carry w c yys xxs
+    (x : xs, y:ys) -> do
+        r <- xor [c,x,y]
+        d <- atleast 2 [c,x,y]
+        rest <- add_with_carry (w-1) d xs ys
+        return $ r : rest
+
+-- | result bit width is at most max of argument bit widths.
+-- if overflow occurs, then formula is unsatisfiable.
+times :: Number -> Number -> SAT Number
+times a b = do 
+    let w = max ( width a ) ( width b ) 
+    restricted_times w a b
+
+restricted_times :: Int -> Number -> Number -> SAT Number
+restricted_times w a b = case bits a of
+    [] -> return $ make []
+    _ | w <= 0 -> do
+        monadic assert [ Flexible.iszero a, Flexible.iszero b ]
+        return $ make []
+    x : xs -> do 
+        xys  <- Flexible.times1 x b
+        xsys <- if null $ bits b 
+                then return $ make [] 
+                else do
+                       zs <- restricted_times (w-1) b (make xs)
+                       Flexible.shift zs
+        s <- Flexible.add xys xsys
+        restricted w s
+
+        
+
+
+
+
diff --git a/Satchmo/Binary/Op/Flexible.hs b/Satchmo/Binary/Op/Flexible.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Binary/Op/Flexible.hs
@@ -0,0 +1,63 @@
+{-# language MultiParamTypeClasses, PatternGuards #-}
+
+-- | operations from this module cannot overflow.
+-- instead they increase the bit width.
+
+module Satchmo.Binary.Op.Flexible
+
+( add, times
+, add_with_carry, times1, shift
+, module Satchmo.Binary.Data
+)
+
+where
+
+import Prelude hiding ( and, or, not )
+
+import Satchmo.Boolean
+import qualified Satchmo.Code as C
+import Satchmo.Binary.Data
+import Satchmo.Counting
+
+add :: Number -> Number -> SAT Number
+add a b = do
+    false <- Satchmo.Boolean.constant False
+    ( zs, carry ) <- add_with_carry false (bits a) (bits b)
+    return $ make $ zs ++ [carry]
+
+add_with_carry :: Boolean 
+               -> Booleans -> Booleans
+               -> SAT ( Booleans, Boolean )
+add_with_carry cin [] [] = return ( [], cin )
+add_with_carry cin (x:xs) [] = do
+    z <- xor [ cin, x ]
+    c <- and [ cin, x ]
+    ( zs, cout ) <- add_with_carry c xs []
+    return ( z : zs, cout )
+add_with_carry cin [] (y:ys) = do
+    add_with_carry cin (y:ys) []
+add_with_carry cin (x:xs ) (y:ys) = do
+    z  <- xor [ cin, x, y ]
+    c <- atleast 2 [ cin, x, y ]
+    ( zs, cout ) <- add_with_carry c xs ys
+    return ( z : zs, cout )
+
+times :: Number -> Number -> SAT Number
+times a b | [x] <- bits a = times1 x b
+times a b | x:xs <- bits a = do
+    xys  <- times1 x b
+    xsys <- times (make xs) b
+    zs <- shift xsys
+    add xys zs
+
+-- | multiply by 2
+shift :: Number -> SAT Number
+shift a = do
+    false <- Satchmo.Boolean.constant False 
+    return $ make $ false : bits a
+
+times1 :: Boolean -> Number -> SAT Number
+times1 x b = do
+    zs <- mapM ( \ y -> and [x,y] ) $ bits b
+    return $ make zs
+
diff --git a/Satchmo/Boolean/Data.hs b/Satchmo/Boolean/Data.hs
--- a/Satchmo/Boolean/Data.hs
+++ b/Satchmo/Boolean/Data.hs
@@ -2,7 +2,8 @@
 
 module Satchmo.Boolean.Data 
 
-( Boolean, boolean, constant
+( Boolean, Booleans
+, boolean, constant
 , not, assert, monadic
 )
 
@@ -28,6 +29,8 @@
              , decode :: C.Decoder Bool
              }
      | Constant { value :: Bool }
+
+type Booleans = [ Boolean ]
 
 isConstant :: Boolean -> Bool
 isConstant ( Constant {} ) = True
diff --git a/TODO b/TODO
--- a/TODO
+++ b/TODO
@@ -1,8 +1,11 @@
 * minisat needs to be in the $PATH (for execution),
-  but this is not checked during installation.
+  this should be checked during installation.
 
-* actually, should provide several backends (separate package satchmo-minisat etc.,
+* should provide several backends (separate package satchmo-minisat etc.,
   similar as hsql with backends like hsql-mysql etc.)
 
-* need timeout handler for calling the SAT solver.
+* add timeout handler for calling the SAT solver.
+  
+
+* implement fixed-width integer arithmetics
 
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo
-Version:        1.0
+Version:        1.1
 License:        GPL
 License-file:	gpl-2.0.txt
 Author:         Johannes Waldmann
@@ -9,21 +9,25 @@
 Synopsis:       SAT encoding monad
 description:	Encoding for boolean and integral constraints into CNF-SAT.
 		The encoder is provided as a State monad (hence the "mo" in "satchmo").
-		Requires SAT solver minisat installed.
+		Requires SAT solver "minisat" installed.
 Build-depends:  mtl, process, containers, base, array
 Exposed-modules:
-        Satchmo.Boolean
         Satchmo.Solve
+        Satchmo.Boolean
 	Satchmo.Counting
-	Satchmo.Binary
 	Satchmo.Code
+	Satchmo.Binary
+	Satchmo.Binary.Op.Fixed
+	Satchmo.Binary.Op.Flexible
 Other-modules:
+	Satchmo.Binary.Data
+        Satchmo.Boolean.Op
         Satchmo.Boolean.Data
-	Satchmo.Boolean.Op
 	Satchmo.Internal
 	Satchmo.Data
 hs-source-dirs:	.
 extra-source-files: test/Binary.hs  test/HC.hs      test/Schur.hs
+		    test/Factor.hs
 		    test/Cage.hs    test/Ramsey.hs  test/VC.hs
 		    TODO
 extensions: 
diff --git a/test/Binary.hs b/test/Binary.hs
--- a/test/Binary.hs
+++ b/test/Binary.hs
@@ -2,14 +2,17 @@
 
 import Prelude hiding ( not )
 
-import Satchmo.Boolean
+import Satchmo.Boolean hiding ( constant )
 import Satchmo.Code
-import Satchmo.Binary
+
+import Satchmo.Binary.Op.Fixed
+-- import Satchmo.Binary.Op.Flexible
+
 import Satchmo.Solve
 
 
 assert_positive x = do 
-    n <- fixed 0 0 
+    n <- constant 0 
     e <- equals n x 
     assert [ not e ]
 
@@ -25,13 +28,13 @@
 
 test1 = do 
     x <- number 4 
-    y <- fixed 4 12 
+    y <- constant 12 
     assert_equals x y
     return $ decode (x,y)
 
 test2 = do 
-    x <- fixed 5 3
-    y <- fixed 5 9
+    x <- constant 3
+    y <- constant 9
     z <- add x y
     return $ decode [x,y,z]
 
@@ -39,7 +42,7 @@
     x <- number 5 
     xx <- add x x
     xxx <- add xx x
-    y <- fixed 5 15 
+    y <- constant 15 
     assert_equals xxx y 
     return $ decode [ x, y ]
 
@@ -47,20 +50,20 @@
     x <- number  8
     y <- number  8
     xy <- times x y
-    z <- fixed 8 63
+    z <- constant 63
     assert_equals xy z
     return $ decode [x, y, z]
 
 test5 = do 
-    x <- number  8
-    y <- number  8
+    x <- number  10
+    y <- number  10
     xy <- times x y
-    z <- fixed 10 1001
+    z <- constant 1001
     assert_equals xy z
     return $ decode [x, y, z]
 
 ramanujan = do
-    let bits = 5
+    let bits = 11
     a <- number  bits
     b <- number  bits
     c <- number  bits
diff --git a/test/Factor.hs b/test/Factor.hs
new file mode 100644
--- /dev/null
+++ b/test/Factor.hs
@@ -0,0 +1,32 @@
+-- | attempt factorization of integer.
+-- | run like this: ./test/Factor 1000000000001
+-- (takes 10 .. 20 seconds depending on your CPU)
+
+import Prelude hiding ( not )
+
+import Satchmo.Binary.Op.Fixed 
+import qualified Satchmo.Binary.Op.Flexible 
+import Satchmo.Solve
+import Satchmo.Boolean 
+import Satchmo.Code
+
+import System.Environment
+
+main :: IO ()
+main = do
+    [ n ] <- getArgs
+    res <- solve $ do
+        x <- Satchmo.Binary.Op.Flexible.constant $ read n
+        a <- number $ width x 
+        notone a
+        b <- number $ width x  
+        notone b
+        ab <- times a b
+        monadic assert [ equals ab x ]
+        return $ decode [ a, b ]
+    print res
+
+notone f = do
+    one <- Satchmo.Binary.Op.Flexible.constant 1
+    e <- equals f one
+    assert [ not e ]
diff --git a/test/VC.hs b/test/VC.hs
--- a/test/VC.hs
+++ b/test/VC.hs
@@ -8,6 +8,7 @@
 
 import Control.Monad ( guard )
 import System.Environment
+import System.Timeout
 
 -- | command line arguments: n s
 -- compute vertex cover of size <= s for knight's graph on  n x n  chess board
@@ -16,7 +17,8 @@
 main = do
     argv <- getArgs
     let [ n, s ] = map read argv
-    Just a <- solve $ knight n s
+    -- this is just to check whether time-outing works
+    Just (Just a) <- timeout (10^6) $ solve $ knight n s
     putStrLn $ table a
 
 knight n s = do