diff --git a/Satchmo/Binary/Op/Times.hs b/Satchmo/Binary/Op/Times.hs
--- a/Satchmo/Binary/Op/Times.hs
+++ b/Satchmo/Binary/Op/Times.hs
@@ -1,5 +1,11 @@
-module Satchmo.Binary.Op.Times where
+module Satchmo.Binary.Op.Times
 
+( times, dot_product
+, Overflow (..), times'
+)
+
+where
+
 import Prelude hiding ( and, or, not )
 
 import Satchmo.Boolean
@@ -9,65 +15,73 @@
 
 import qualified Data.Map as M
 import Control.Monad ( forM )
-
+import Control.Applicative
 
 dot_product :: (MonadSAT m) 
              => ( Maybe Int) 
             -> [ Number ] -> [ Number ] -> m Number
 dot_product bound xs ys = do
-    cs <- forM ( zip xs ys ) $ \ (x,y) -> product_components bound x y
-    export bound $ concat cs
+    cs <- forM ( zip xs ys ) $ \ (x,y) -> product_components Refuse bound (bits x) (bits y)
+    make <$> export Refuse bound ( concat cs )
 
+data Overflow = Ignore | Refuse
+
 times :: (MonadSAT m) 
              => Maybe Int
              -> Number -> Number -> m Number
-times bound a b = do
-    kzs <- product_components bound a b
-    export bound kzs
+times bound a b =
+  make <$> times' Refuse bound (bits a) (bits b)
 
-product_components :: MonadSAT m
-    => Maybe Int
-    -> Number -> Number -> m [ (Int, [Boolean]) ]
-product_components bound a b = sequence $ do
-    ( i , x ) <- zip [ 0 .. ] $ bits a
-    ( j , y ) <- zip [ 0 .. ] $ bits b        
+times' over bound a b = do
+    kzs <- product_components over bound a b
+    export over bound kzs
+
+product_components over bound a b = sequence $ do
+    ( i , x ) <- zip [ 0 .. ] a
+    ( j , y ) <- zip [ 0 .. ] b        
     return $ do
         z <- and [ x, y ]
         if ( case bound of Nothing -> False ; Just b -> i+j >= b )
-             then do assert [ not z ] ; return ( i+j , [ ] )
-             else do                    return ( i+j , [z] ) 
+             then do
+                case over of
+                  Ignore -> return ()
+                  Refuse -> assert [ not z ]
+                return ( i+j , [ ] )
+             else do
+                return ( i+j , [z] ) 
 
-export :: MonadSAT m => Maybe Int -> [(Int,[Boolean])] -> m Number
-export bound kzs = do 
-    m <- reduce bound $ M.fromListWith (++) kzs
+export over bound kzs = do 
+    m <- reduce over bound $ M.fromListWith (++) kzs
     case M.maxViewWithKey m of
-        Nothing -> return $ make []
+        Nothing -> return []
         Just ((k,_) , _) -> do 
-              return $ make $ do 
+              return $ do 
                     i <- [ 0 .. k ] 
                     let { [ b ] = m M.! i }  
                     return b
 
-reduce bound m = case M.minViewWithKey m of
+reduce over bound m = case M.minViewWithKey m of
     Nothing -> return M.empty
     Just ((k, bs), rest ) -> 
         if ( case bound of Nothing -> False ; Just b -> k >= b )
         then do
-            forM bs $ \ b -> assert [ not b ]
-            reduce bound rest
+            forM bs $ \ b -> case over of
+              Refuse -> assert [ not b ]
+              Ignore -> return ()
+            reduce over bound rest
         else case bs of
-            [] -> reduce bound rest
+            [] -> reduce over bound rest
             [x] -> do
-                m' <- reduce bound rest
+                m' <- reduce over bound rest
                 return $ M.unionWith (error "huh") m' 
                        $ M.fromList [(k,[x])] 
             [x,y] -> do
                 (r,c) <- half_adder x y
-                reduce bound $ M.unionWith (++) rest
+                reduce over bound $ M.unionWith (++) rest
                        $ M.fromList [ (k,[r]), (k+1, [c]) ] 
             (x:y:z:more) -> do
                 (r,c) <- full_adder x y z
-                reduce bound $ M.unionWith (++) rest
+                reduce over bound $ M.unionWith (++) rest
                        $ M.fromList [ (k, more ++ [r]), (k+1, [c]) ] 
 
 
diff --git a/Satchmo/Counting.hs b/Satchmo/Counting.hs
--- a/Satchmo/Counting.hs
+++ b/Satchmo/Counting.hs
@@ -1,59 +1,11 @@
-module Satchmo.Counting 
-
-( atleast
-, atmost
-, exactly
-)
-
-where
-
-import Prelude hiding ( and, or, not )
-
-import Satchmo.Boolean
-
-import Satchmo.SAT ( SAT) -- for specializations
-
-{-# specialize inline atleast :: Int -> [ Boolean] -> SAT Boolean #-}
-{-# specialize inline atmost  :: Int -> [ Boolean] -> SAT Boolean #-}
-{-# specialize inline exactly :: Int -> [ Boolean] -> SAT Boolean #-}
+-- | Re-exports @Satchmo.Counting.Unary@
+-- for backwards compatibility.
 
-atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
-atleast k xs = fmap not $ atmost (k-1) xs
-        
+module Satchmo.Counting
 
-atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
-atmost_block k [] = do
-    t <- constant $ True
-    return $ replicate (k+1) t
-atmost_block k (x:xs) = do
-    cs <- atmost_block k xs
-    f <- constant False
-    sequence $ do
-        (p,q) <- zip cs ( f : cs )
-        return $ do
-            fun3  ( \ x p q -> if x then q else p ) x p q
+( module Satchmo.Counting.Unary )
 
-atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
-atmost k xs = do
-    cs <- atmost_block k xs
-    return $ cs !! k
-        
+where
 
-exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
-exactly_block k [] = do
-    t <- constant True
-    f <- constant False
-    return $ t : replicate k f
-exactly_block k (x:xs) = do
-    f <- constant False
-    cs <- exactly_block k xs
-    sequence $ do
-        (p,q) <- zip cs ( f : cs )
-        return $ do
-            fun3 ( \ x p q -> if x then q else p ) x p q
+import Satchmo.Counting.Unary
 
-exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
-exactly k xs = do
-    cs <- exactly_block k xs
-    return $ cs !! k
-        
diff --git a/Satchmo/Counting/Binary.hs b/Satchmo/Counting/Binary.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Counting/Binary.hs
@@ -0,0 +1,51 @@
+module Satchmo.Counting.Binary
+
+( atleast
+, atmost
+, exactly
+, count
+)
+
+where
+
+import Prelude hiding ( and, or, not )
+
+import Satchmo.Boolean
+import Satchmo.Binary
+
+import Satchmo.SAT ( SAT) -- for specializations
+
+{-# specialize inline atleast :: Int -> [ Boolean] -> SAT Boolean #-}
+{-# specialize inline atmost  :: Int -> [ Boolean] -> SAT Boolean #-}
+{-# specialize inline exactly :: Int -> [ Boolean] -> SAT Boolean #-}
+{-# specialize inline count :: [ Boolean] -> SAT Number #-}
+
+count :: MonadSAT m => [ Boolean ] -> m Number
+count bits
+  = collect (Satchmo.Binary.constant 0) Satchmo.Binary.add
+  $ map ( \ bit -> Satchmo.Binary.make [bit] )
+  $ bits
+
+collect :: Monad m => m a -> (a -> a -> m a) -> [a] -> m a
+collect z b xs = case xs of
+  [] -> z
+  [x] -> return x
+  (x:y:zs) -> b x y >>= \ c -> collect z b (zs ++ [c])
+    
+atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+atleast k xs = common ge k xs
+
+atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+atmost k xs = common le k xs
+        
+exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+exactly k xs = common eq k xs
+
+common :: MonadSAT m
+       => (Number -> Number -> m b)
+       -> Int -> [ Boolean ] -> m b
+common cmp k xs = do
+  c <- count xs
+  goal <- Satchmo.Binary.constant $ fromIntegral k
+  cmp c goal 
+
diff --git a/Satchmo/Counting/Unary.hs b/Satchmo/Counting/Unary.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Counting/Unary.hs
@@ -0,0 +1,59 @@
+module Satchmo.Counting.Unary
+
+( atleast
+, atmost
+, exactly
+)
+
+where
+
+import Prelude hiding ( and, or, not )
+
+import Satchmo.Boolean
+
+import Satchmo.SAT ( SAT) -- for specializations
+
+{-# specialize inline atleast :: Int -> [ Boolean] -> SAT Boolean #-}
+{-# specialize inline atmost  :: Int -> [ Boolean] -> SAT Boolean #-}
+{-# specialize inline exactly :: Int -> [ Boolean] -> SAT Boolean #-}
+
+atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+atleast k xs = fmap not $ atmost (k-1) xs
+        
+
+atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
+atmost_block k [] = do
+    t <- constant $ True
+    return $ replicate (k+1) t
+atmost_block k (x:xs) = do
+    cs <- atmost_block k xs
+    f <- constant False
+    sequence $ do
+        (p,q) <- zip cs ( f : cs )
+        return $ do
+            fun3  ( \ x p q -> if x then q else p ) x p q
+
+atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+atmost k xs = do
+    cs <- atmost_block k xs
+    return $ cs !! k
+        
+
+exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
+exactly_block k [] = do
+    t <- constant True
+    f <- constant False
+    return $ t : replicate k f
+exactly_block k (x:xs) = do
+    f <- constant False
+    cs <- exactly_block k xs
+    sequence $ do
+        (p,q) <- zip cs ( f : cs )
+        return $ do
+            fun3 ( \ x p q -> if x then q else p ) x p q
+
+exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+exactly k xs = do
+    cs <- exactly_block k xs
+    return $ cs !! k
+        
diff --git a/Satchmo/Integer/Data.hs b/Satchmo/Integer/Data.hs
--- a/Satchmo/Integer/Data.hs
+++ b/Satchmo/Integer/Data.hs
@@ -3,8 +3,8 @@
 module Satchmo.Integer.Data 
 
 ( Number, make, number
-, constant
-, bits, width
+, constant, decode
+, bits, width, sign
 )
 
 where
@@ -18,6 +18,7 @@
 import qualified  Satchmo.Boolean as B
 
 import Satchmo.Counting
+import Control.Monad
 
 data Number = Number 
             { bits :: [ Boolean ] -- ^ lsb first,
@@ -30,6 +31,11 @@
 width :: Number -> Int
 width n = length $ bits n
 
+sign :: Number -> Boolean
+sign n = case bits n of
+  [] -> error "Satchmo.Integer.Data:sign no bits"
+  bs -> last bs
+
 -- | declare a number variable (bit width)
 number :: MonadSAT m => Int -> m Number
 number w = do
@@ -64,3 +70,7 @@
     z <- B.constant False
     return $ make $ take w $ xs ++ repeat z
 
+decode w n = do
+  bs <- forM (bits n) C.decode
+  return $ fromBinary bs
+         - if last bs then 2^w else 0
diff --git a/Satchmo/Integer/Op.hs b/Satchmo/Integer/Op.hs
--- a/Satchmo/Integer/Op.hs
+++ b/Satchmo/Integer/Op.hs
@@ -16,6 +16,7 @@
 
 import qualified Satchmo.Binary.Op.Common as C
 import qualified Satchmo.Binary.Op.Flexible as F
+import qualified Satchmo.Binary.Op.Times as T
 
 import Control.Monad ( forM, when )
 
@@ -38,14 +39,19 @@
 add :: MonadSAT m 
     => Number -> Number 
     -> m Number
-add a b = do
-    when ( width a /= width b ) 
-    	 $ error "Satchmo.Integer.Op.add"
+add a0 b0 = do
+
+    let w = max (width a0) (width b0)
+        a = sextn w a0 ; b = sextn w b0
+
     cin <- B.constant False
     ( zs, cout ) <- 
         F.add_with_carry cin ( bits a ) ( bits b )
-    monadic assertOr [ fun2 (==) cout $ last zs ]
-    return $ make zs
+    let c = make zs
+    sab <- B.fun2 (==) (sign a) (sign b)
+    sac <- B.fun2 (==) (sign a) (sign c)
+    B.assert [ B.not sab , sac ]
+    return c
 
 sub :: MonadSAT m 
     => Number -> Number 
@@ -56,17 +62,58 @@
     c <- negate b
     add a c
 
+sextn w n = make $ sext n w
+
 times :: MonadSAT m 
     => Number -> Number 
     -> m Number
-times a b = do
+times a0 b0 = do
+
+    let w = max (width a0) (width b0)
+        a = sextn w a0 ; b = sextn w b0
+        
+    cs <- T.times' T.Ignore (Just w) (bits a) (bits b)
+
+    nza <- or $ bits a ; nzb <- or $ bits b
+    result_should_be_nonzero <- and [ nza, nzb ]
+    result_is_nonzero <- or cs
+
+    assert [ not result_should_be_nonzero, result_is_nonzero ]
+
+    xs <- forM (bits a) $ \ x -> fun2 (/=) x (sign a)
+    ys <- forM (bits b) $ \ y -> fun2 (/=) y (sign b)
+    
+    forM (zip [0..w-2] xs) $ \ (i,x) ->
+      forM (zip [0..w-2] ys) $ \ (j,y) ->
+        when (i+j>=w-1) $ assert [ not x, not y ]
+
+    let c = make cs
+
+    s <- fun2 (/=) (sign a) (sign b)
+    ok <- fun2 (==) s (sign c)
+    
+    assert [ not result_is_nonzero, ok ]
+    
+    return c
+
+-- | inefficient (used double-bit width computation)
+times_model :: MonadSAT m 
+    => Number -> Number 
+    -> m Number
+times_model a b = do
     when ( width a /= width b ) 
     	 $ error "Satchmo.Integer.Op.times"
-    c <- F.times ( F.make $ bits a ) 
-      	 	 ( F.make $ bits b )
-    let ( pre, post ) = splitAt ( width a ) $ F.bits c
-    monadic assertOr [ fun2 (==) ( head post) $ last pre ]
-    return $ make pre
+    let w = width a
+    cs <- T.times' T.Ignore (Just (2*w)) (sext a w) (sext b w)
+    let (small, large) = splitAt w cs
+    allone <- B.and large ; allzero <- B.and ( map B.not large )
+    B.assert [ allone, allzero ]
+    e <- B.fun2 (==) (last small) (head large)
+    B.assert[e]
+    return $ make small
+
+sext a w = bits a ++ replicate (w - width a) (sign a)
+    
 
 ----------------------------------------------------
 
diff --git a/Satchmo/Map/Data.hs b/Satchmo/Map/Data.hs
--- a/Satchmo/Map/Data.hs
+++ b/Satchmo/Map/Data.hs
@@ -4,6 +4,8 @@
 module Satchmo.Map.Data
 
 ( Map
+, unknown, constant
+, (!), 
 ) 
 
 where
@@ -20,6 +22,8 @@
 import Control.Applicative ( (<$>), (<*>) )
 
 newtype Map a b = Map (M.Map a b)
+
+Map m ! i = m M.! i
 
 instance ( Functor m, Decode m b c, Ord a )
          => Decode m (Map a b) ( M.Map a c) where
diff --git a/Satchmo/Set/Data.hs b/Satchmo/Set/Data.hs
--- a/Satchmo/Set/Data.hs
+++ b/Satchmo/Set/Data.hs
@@ -18,8 +18,6 @@
 import qualified Data.Set as S
 import qualified Data.Map.Strict as M
 
-import Satchmo.Map
-
 import Control.Monad ( guard, forM )
 import Control.Applicative ( (<$>), (<*>) )
 import Data.List ( tails )
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo
-Version:        2.8.2
+Version:        2.9.0
 
 License:        GPL
 License-file:	gpl-2.0.txt
@@ -28,6 +28,8 @@
         -- Satchmo.Solve
         Satchmo.Boolean
         Satchmo.Counting
+        Satchmo.Counting.Unary
+        Satchmo.Counting.Binary
         Satchmo.Code
         Satchmo.Integer
         Satchmo.Binary