diff --git a/picologic.cabal b/picologic.cabal
--- a/picologic.cabal
+++ b/picologic.cabal
@@ -1,5 +1,5 @@
 name:                picologic
-version:             0.1
+version:             0.1.1
 synopsis:            Utilities for symbolic predicate logic expressions
 homepage:            https://github.com/sdiehl/picologic
 license:             MIT
@@ -32,7 +32,7 @@
   hs-source-dirs:      src
   other-extensions:    DeriveDataTypeable, BangPatterns
   build-depends:       
-    base        >= 4.6 && <4.7,
+    base        >= 4.6 && <4.8,
     picosat     >= 0.1 && <0.2,
     containers  >= 0.5 && <0.6,
     mtl         >= 2.1 && <2.2,
@@ -47,7 +47,7 @@
     other-modules: Picologic.Repl
     other-extensions:    DeriveDataTypeable, BangPatterns
     build-depends:       
-      base        >= 4.6 && <4.7,
+      base        >= 4.6 && <4.8,
       picosat     >= 0.1 && <0.2,
       containers  >= 0.5 && <0.6,
       mtl         >= 2.1 && <2.2,
diff --git a/src/Picologic/AST.hs b/src/Picologic/AST.hs
--- a/src/Picologic/AST.hs
+++ b/src/Picologic/AST.hs
@@ -20,7 +20,6 @@
 import Data.Maybe
 import qualified Data.Map as M
 
-
 newtype Ident = Ident String
   deriving (Eq, Ord, Show, Data, Typeable)
 
diff --git a/src/Picologic/Solver.hs b/src/Picologic/Solver.hs
--- a/src/Picologic/Solver.hs
+++ b/src/Picologic/Solver.hs
@@ -7,7 +7,7 @@
 import Picosat
 
 import Data.List
-import Data.Map as M
+import qualified Data.Map as M
 import Control.Monad.Writer
 
 data Clause
@@ -22,19 +22,19 @@
 solveProp :: Expr -> IO Solutions
 solveProp p = solveAll cs >>= return . Solutions . fmap (backSubst vs')
   where
-    cs = fmap toInts $ execWriter $ clauses vs (cnf p)
+    cs = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)
     vs  = M.fromList $ zip vars [1..]
     vs' = M.fromList $ zip [1..] vars
     vars = variables (cnf p)
 
 -- | Yield the integer clauses given to the SAT solver.
 clausesExpr :: Expr -> [[Int]]
-clausesExpr p = fmap toInts $ execWriter $ clauses vs (cnf p)
+clausesExpr p = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)
   where
     vs = M.fromList $ zip vars [1..]
     vars = variables (cnf p)
 
-backSubst :: Map Int Ident -> Solution -> [Expr]
+backSubst :: M.Map Int Ident -> Solution -> [Expr]
 backSubst env (Solution xs) = fmap go xs
   where
     go x | x >= 0 = Var (env M.! x)
@@ -44,6 +44,7 @@
 
 toInts :: Clause -> [Int]
 toInts (CL xs) = fmap (\(CV n) -> n) xs
+toInts (CV x) = [x]
 
 neg :: Clause -> Clause
 neg (CV n) = CV (-n)
@@ -64,10 +65,9 @@
   Conj e1 e2 -> do
     cs1 <- clauses env e1
     cs2 <- clauses env e2
-    tell [combine cs1 cs2]
-    return (combine cs1 cs2)
+    tell [cs1, cs2]
+    return (CL [])
   Disj e1 e2 -> do
     cs1 <- clauses env e1
     cs2 <- clauses env e2
-    tell [combine cs1 cs2]
     return (combine cs1 cs2)