diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,5 +1,5 @@
 name:                liquid-fixpoint
-version:             0.2.1.0
+version:             0.2.1.1
 Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
@@ -92,7 +92,7 @@
 -- asked.
 Executable fixpoint.native
   Main-is: Fixpoint.hs
-  Build-Depends: base >= 4 && < 5
+  Build-Depends: base >= 4.7 && < 5
                , array
                , syb
                , cmdargs
@@ -118,7 +118,7 @@
 
 Executable fixpoint
   Main-is:       Fixpoint.hs
-  Build-Depends: base >= 4 && < 5
+  Build-Depends: base >= 4.7 && < 5
                , array
                , syb
                , cmdargs
@@ -156,7 +156,7 @@
                    Language.Fixpoint.SmtLib2,
                    Language.Fixpoint.Misc
   
-  Build-Depends: base >= 4 && < 5
+  Build-Depends: base >= 4.7 && < 5
                , array
                , attoparsec
                , syb
diff --git a/src/Language/Fixpoint/SmtLib2.hs b/src/Language/Fixpoint/SmtLib2.hs
--- a/src/Language/Fixpoint/SmtLib2.hs
+++ b/src/Language/Fixpoint/SmtLib2.hs
@@ -44,9 +44,7 @@
 import Language.Fixpoint.Files
 import Language.Fixpoint.Types
 
-import Control.Arrow
 import Control.Monad
-import Control.Monad.IO.Class
 import Data.Char
 import qualified Data.List as L
 import qualified Data.HashMap.Strict as M
@@ -60,13 +58,9 @@
 import System.Exit
 import System.FilePath
 import System.Process
-import System.IO            (openFile, IOMode (..), Handle, hFlush, hClose, hReady)
+import System.IO            (openFile, IOMode (..), Handle, hFlush, hClose)
 import Control.Applicative  ((<$>), (<|>), (*>), (<*))
 
-import Text.Parsec.Text.Lazy ()
-import Text.Parsec.Char
-import Text.Parsec.Combinator
-import Text.Parsec.Prim (ParsecT, runPT, getState, setInput, try)
 import qualified Data.Attoparsec.Text as A
 
 {- Usage:
@@ -248,9 +242,9 @@
 smtPreamble Z3 me 
   = do smtWrite me "(get-info :version)"
        r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me
-       case r of
-         "4.3.2" -> return $ z3_432_options ++ z3Preamble
-         _       -> return $ z3_options ++ z3Preamble
+       case T.words r of
+         "4.3.2" : _  -> return $ z3_432_options ++ z3Preamble
+         _            -> return $ z3_options ++ z3Preamble
 smtPreamble _  _  
   = return smtlibPreamble
 
diff --git a/src/Language/Fixpoint/Sort.hs b/src/Language/Fixpoint/Sort.hs
--- a/src/Language/Fixpoint/Sort.hs
+++ b/src/Language/Fixpoint/Sort.hs
@@ -149,9 +149,7 @@
   = do tp <- checkPred f p
        t1 <- checkExpr f e1
        t2 <- checkExpr f e2
-       if t1 == t2 
-         then return t1
-         else throwError (errIte e1 e2 t1 t2) 
+       ((`apply` t1) <$> unify [t1] [t2]) `catchError` (\_ -> throwError $ errIte e1 e2 t1 t2)
 
 -- | Helper for checking cast expressions 
 
@@ -159,10 +157,7 @@
   = checkApp f (Just t) g es
 checkCst f t e           
   = do t' <- checkExpr f e
-       if t == t' 
-         then return t
-         else throwError (errCast e t' t)
-
+       ((`apply` t) <$> unify [t] [t']) `catchError` (\_ -> throwError $ errCast e t' t)
 
 checkApp f to g es
   = snd <$> checkApp' f to g es
diff --git a/src/Language/Fixpoint/Types.hs b/src/Language/Fixpoint/Types.hs
--- a/src/Language/Fixpoint/Types.hs
+++ b/src/Language/Fixpoint/Types.hs
@@ -63,6 +63,7 @@
   , pAnd, pOr, pIte
   , isTautoPred
   , symConstLits
+  , zero
 
   -- * Generalizing Embedding with Typeclasses
   , Symbolic (..)
@@ -647,6 +648,7 @@
 exprReft      = relReft Eq
 notExprReft   = relReft Ne
 uexprReft     = relReft Ueq
+
 
 -- exprReft e             = Reft (vv_, [RConc $ PAtom Eq (eVar vv_)  (expr e)])
 -- notExprReft e          = Reft (vv_, [RConc $ PAtom Ne (eVar vv_)  (expr e)])