diff --git a/Satchmo/Binary/Data.hs b/Satchmo/Binary/Data.hs
--- a/Satchmo/Binary/Data.hs
+++ b/Satchmo/Binary/Data.hs
@@ -4,7 +4,6 @@
 
 ( Number, bits, make
 , width, number, constant
-, equals, iszero
 )
 
 where
@@ -55,20 +54,4 @@
 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/Common.hs b/Satchmo/Binary/Op/Common.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Binary/Op/Common.hs
@@ -0,0 +1,50 @@
+module Satchmo.Binary.Op.Common
+
+( iszero
+, equals
+, full_adder, half_adder
+)
+
+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.Binary.Data
+
+import Satchmo.Counting
+
+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
+
+full_adder :: Boolean -> Boolean -> Boolean
+           -> SAT ( Boolean, Boolean )
+full_adder a b c = do
+    let s x y z = sum $ map fromEnum [x,y,z]
+    r <- fun3 ( \ x y z -> odd $ s x y z ) a b c
+    d <- fun3 ( \ x y z -> 1   < s x y z ) a b c
+    return ( r, d )
+
+half_adder :: Boolean -> Boolean 
+           -> SAT ( Boolean, Boolean )
+half_adder a b = do
+    let s x y = sum $ map fromEnum [x,y]
+    r <- fun2 ( \ x y -> odd $ s x y ) a b
+    d <- fun2 ( \ x y -> 1   < s x y ) a b
+    return ( r, d )
diff --git a/Satchmo/Binary/Op/Fixed.hs b/Satchmo/Binary/Op/Fixed.hs
--- a/Satchmo/Binary/Op/Fixed.hs
+++ b/Satchmo/Binary/Op/Fixed.hs
@@ -11,6 +11,7 @@
 ( restricted
 , add, times
 , module Satchmo.Binary.Data
+, module Satchmo.Binary.Op.Common
 )
 
 where
@@ -21,6 +22,7 @@
 
 import Satchmo.Boolean
 import Satchmo.Binary.Data
+import Satchmo.Binary.Op.Common
 import qualified Satchmo.Binary.Op.Flexible as Flexible
 
 import Satchmo.Counting
@@ -49,14 +51,16 @@
         return []
     ( [] , [] ) -> return [ c ]
     ( [], y : ys) -> do
-        r <- xor [ c, y ]
-        d <- and [ c, y ]
+        -- r <- xor [ c, y ]
+        -- d <- and [ c, y ]
+        (r,d) <- half_adder 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]
+        -- r <- xor [c,x,y]
+        -- d <- atleast 2 [c,x,y]
+        (r,d) <- full_adder c x y
         rest <- add_with_carry (w-1) d xs ys
         return $ r : rest
 
diff --git a/Satchmo/Binary/Op/Flexible.hs b/Satchmo/Binary/Op/Flexible.hs
--- a/Satchmo/Binary/Op/Flexible.hs
+++ b/Satchmo/Binary/Op/Flexible.hs
@@ -8,6 +8,7 @@
 ( add, times
 , add_with_carry, times1, shift
 , module Satchmo.Binary.Data
+, module Satchmo.Binary.Op.Common
 )
 
 where
@@ -17,6 +18,7 @@
 import Satchmo.Boolean
 import qualified Satchmo.Code as C
 import Satchmo.Binary.Data
+import Satchmo.Binary.Op.Common
 import Satchmo.Counting
 
 add :: Number -> Number -> SAT Number
@@ -30,15 +32,17 @@
                -> SAT ( Booleans, Boolean )
 add_with_carry cin [] [] = return ( [], cin )
 add_with_carry cin (x:xs) [] = do
-    z <- xor [ cin, x ]
-    c <- and [ cin, x ]
+    -- z <- xor [ cin, x ]
+    -- c <- and [ cin, x ]
+    (z, c) <- half_adder 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 ]
+    -- z  <- xor [ cin, x, y ]
+    -- c <- atleast 2 [ cin, x, y ]
+    (z, c) <- full_adder cin x y
     ( zs, cout ) <- add_with_carry c xs ys
     return ( z : zs, cout )
 
diff --git a/Satchmo/Boolean/Op.hs b/Satchmo/Boolean/Op.hs
--- a/Satchmo/Boolean/Op.hs
+++ b/Satchmo/Boolean/Op.hs
@@ -2,17 +2,21 @@
 
 ( constant
 , and, or, xor
+, fun2, fun3
 , monadic
 )
 
 where
 
 import Prelude hiding ( and, or, not )
+import qualified Prelude
 
 import Satchmo.Internal
 import Satchmo.Code
 import Satchmo.Boolean.Data
 
+import Control.Monad ( foldM )
+
 and :: [ Boolean ] -> SAT Boolean
 and xs = do
     y <- boolean
@@ -28,14 +32,51 @@
     return $ not y
 
 xor :: [ Boolean ] -> SAT Boolean
-xor [x] = return x
-xor (x : xs) = do
-    rest <- xor xs
-    xor2 x rest
+xor [] = constant False
+xor (x:xs) = foldM xor2 x xs
 
+
+-- | implement the function by giving a full CNF
+-- that determines the outcome
+fun2 :: ( Bool -> Bool -> Bool )
+     -> Boolean -> Boolean 
+     -> SAT Boolean
+fun2 f x y = do
+    r <- boolean
+    sequence_ $ do
+        a <- [ False, True ]
+        b <- [ False, True ]
+        let pack flag var = if flag then not var else var
+        return $ assert 
+            [ pack a x, pack b y, pack (Prelude.not $ f a b) r ]
+    return r
+
+-- | implement the function by giving a full CNF
+-- that determines the outcome
+fun3 :: ( Bool -> Bool -> Bool -> Bool )
+     -> Boolean -> Boolean -> Boolean
+     -> SAT Boolean
+fun3 f x y z = do
+    r <- boolean
+    sequence_ $ do
+        a <- [ False, True ]
+        b <- [ False, True ]
+        c <- [ False, True ]
+        let pack flag var = if flag then not var else var
+        return $ assert 
+            [ pack a x, pack b y, pack c z
+            , pack (Prelude.not $ f a b c) r 
+            ]
+    return r
+
 xor2 :: Boolean -> Boolean -> SAT Boolean
-xor2 x y = do
+xor2 = fun2 (/=)
+
+-- for historic reasons:
+xor2_orig :: Boolean -> Boolean -> SAT Boolean
+xor2_orig x y = do
     a <- and [ x, not y ]
     b <- and [ not x, y ]
     or [ a, b ]
+
 
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo
-Version:        1.1.1
+Version:        1.2
 License:        GPL
 License-file:	gpl-2.0.txt
 Author:         Johannes Waldmann
@@ -16,6 +16,7 @@
 	Satchmo.Counting
 	Satchmo.Code
 	Satchmo.Binary
+	Satchmo.Binary.Op.Common
 	Satchmo.Binary.Op.Fixed
 	Satchmo.Binary.Op.Flexible
 Other-modules:
diff --git a/test/Binary.hs b/test/Binary.hs
--- a/test/Binary.hs
+++ b/test/Binary.hs
@@ -1,4 +1,4 @@
--- | run tests like this: "solve test2"
+-- | run tests (in ghci) like this: "solve test2"
 
 import Prelude hiding ( not )
 
diff --git a/test/VC.hs b/test/VC.hs
--- a/test/VC.hs
+++ b/test/VC.hs
@@ -18,12 +18,15 @@
     argv <- getArgs
     let [ n, s ] = map read argv
     -- this is just to check whether time-outing works
-    Just (Just a) <- timeout (10^6) $ solve $ knight n s
+    -- Just (Just a) <- timeout (10^6) $ solve $ knight n s
+
+    Just a <- solve $ knight n s
     putStrLn $ table a
 
 knight n s = do
     a <- relation ((1,1),(n,n))
-    m <- atmost s $ do i <- indices a ; return $ a ! i
+    m <- atmost s $ do 
+           i <- indices a ; return $ a ! i
     assert [m]
     sequence_ $ do
         p <- indices a