diff --git a/.gitignore b/.gitignore
index 2647b48ccfecca56ced11e59611a53ed44410b8b..77c94768e4622647b2921ddc87f91a73b4a6a8e5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,3 +12,5 @@ tests/org/
 .stack-work/
 # Intellij IDEA
 .idea/
+# Z3
+z3.log
diff --git a/app/Main.hs b/app/Main.hs
index 9687543d061e46233d937d6510c0568e0ee6e397..4aac103e93e41d3722f843ff0847149b611dc6e1 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -3,16 +3,16 @@ module Main where
 import Control.Monad
 import Data.Semigroup ((<>))
 import Options.Applicative
-import API (compareSpec, Mode (..), ParseMode (..))
 
+import API (Mode (..), ParseMode (..), compareSpec)
 import Server (runApi)
 
 -- | Command-line options.
 data Options = Options
-  { srcA      :: String
-  , srcB      :: String
-  , method1   :: String
-  , method2   :: String
+  { sourceA   :: String
+  , sourceB   :: String
+  , methodA   :: String
+  , methodB   :: String
   , runServer :: Bool
   , port      :: Int
   }
@@ -69,10 +69,10 @@ main = runMain =<< execParser (parseOptions `withInfo` "Java WLP")
 
 -- | Run.
 runMain :: Options -> IO ()
-runMain (Options srcA srcB methodA methodB runServer port) =
-  if runServer then
-    runApi port
+runMain (Options srcA srcB methA methB serverFlag portNo) =
+  if serverFlag then
+    runApi portNo
   else do
-    when (methodA == "_default_") $ fail "No files given."
-    response <- compareSpec Release File (srcA, methodA) (srcB, methodB)
+    when (methA == "_default_") $ fail "No files given."
+    response <- compareSpec Release File (srcA, methA) (srcB, methB)
     print response
diff --git a/javawlp.cabal b/javawlp.cabal
index 8aed0714e1ff07654b277ffa8e5e76a7d2269629..b2eb9801f0edf395677ea2f0a0d4458ab1556d87 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -74,8 +74,9 @@ library
                      , text
                      , http-types
                      , lens
+                     , deepseq
   default-language:    Haskell2010
-  ghc-options:         -Wall
+  -- ghc-options:         -Wall
 
 test-suite javawlp-tests
   type:                exitcode-stdio-1.0
diff --git a/src/API.hs b/src/API.hs
index 95afb88dcfdb2fd1352938d88494b7a16ba05b92..56724a7464de321b7abbbbb9577da277e2a5094e 100644
--- a/src/API.hs
+++ b/src/API.hs
@@ -1,7 +1,9 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 module API where
 
 import Control.Concurrent
 import Data.Maybe
+import Data.List.Split (splitOn)
 
 import Javawlp.Engine.HelperFunctions
 import Javawlp.Engine.Types
@@ -14,6 +16,9 @@ import LogicIR.Frontend.Java (javaExpToLExpr)
 import LogicIR.Null (lExprPreprocessNull)
 import Model
 
+import Control.DeepSeq
+import Control.Exception.Base
+
 -- | Data types.
 data Mode = Debug | Release deriving (Eq, Show)
 
@@ -66,11 +71,19 @@ getRes Debug    resp              resp'             =
 checkSpec :: ParseMode -> EquivImpl -> (Source, String) -> (FilePath, String) -> IO Response
 checkSpec pMode equivTo methodA methodB = do
     [m1, m2] <- mapM (parseMethod pMode) [methodA, methodB]
-    let (preL, preL') = methodDefToLExpr m1 m2 "pre"
-    preRes <- preL `equivTo` preL'
-    let (postL, postL') = methodDefToLExpr m1 m2 "post"
-    postRes <- postL `equivTo` postL'
-    return $ preRes <> postRes
+    res <- methodDefToLExpr m1 m2 "pre"
+    case res of
+      Left e ->
+        return $ ErrorResponse $ head $ splitOn "CallStack" e
+      Right (preL, preL') -> do
+        preRes <- preL `equivTo` preL'
+        res' <- methodDefToLExpr m1 m2 "post"
+        case res' of
+          Left e' ->
+            return $ ErrorResponse e'
+          Right (postL, postL') -> do
+            postRes <- postL `equivTo` postL'
+            return $ preRes <> postRes
 
 --------------------------------------------------------------------------------
 
@@ -88,16 +101,19 @@ parseMethod pMode (src, name) = do
     -- return the relevant data
     return (decls, mbody, env)
 
-methodDefToLExpr :: MethodDef -> MethodDef -> String -> (LExpr, LExpr)
+methodDefToLExpr :: MethodDef -> MethodDef -> String -> IO (Either String (LExpr, LExpr))
 methodDefToLExpr m1@(decls1, _, env1) m2@(decls2, _, env2) name = do
     -- get pre/post condition
     let (e1, e2) = (extractCond m1 name, extractCond m2 name)
-    let (l1, l2) = (javaExpToLExpr e1 env1 decls1, javaExpToLExpr e2 env2 decls2)
-    -- preprocess "a == null" to "isNull(a)"
-    let (l, l') = (lExprPreprocessNull l1, lExprPreprocessNull l2)
-    (l, l')
-        where extractCond :: MethodDef -> String -> Exp
-              extractCond m n = extractExpr $ getMethodCalls m n
+    res :: Either SomeException (LExpr, LExpr) <-
+      try . evaluate . force $ (javaExpToLExpr e1 env1 decls1, javaExpToLExpr e2 env2 decls2)
+    return $ case res of
+      Left e ->
+        Left $ show e
+      Right (l, l') ->
+        Right (lExprPreprocessNull l, lExprPreprocessNull l')
+    where extractCond :: MethodDef -> String -> Exp
+          extractCond m n = extractExpr $ getMethodCalls m n
 
 -- Get a list of all calls to a method of a specific name from a method definition.
 getMethodCalls :: MethodDef -> String -> [MethodInvocation]
diff --git a/src/LogicIR/Backend/Z3/API.hs b/src/LogicIR/Backend/Z3/API.hs
index cce27f738e08c4bb75ea95862a5428f9455c926f..f761068873902f7cf6d893f09d9316f13df5442c 100644
--- a/src/LogicIR/Backend/Z3/API.hs
+++ b/src/LogicIR/Backend/Z3/API.hs
@@ -1,20 +1,17 @@
 module LogicIR.Backend.Z3.API where
 
-import Z3.Monad hiding (Model)
 import qualified Z3.Base as Z3
-import Z3.Opts
+import Z3.Monad hiding (Model)
 
-import Data.String
 import Control.Exception.Base (tryJust)
-import Control.Monad (forM, forM_, when)
-import Control.Monad.Trans (liftIO)
+import Control.Monad (forM)
+import Data.String
 import Data.Maybe (fromJust)
-import Data.Monoid ((<>))
 import qualified Data.Map as M
 
-import Model
-import LogicIR.Expr (LExpr)
 import LogicIR.Backend.Z3.Z3
+import LogicIR.Expr (LExpr)
+import Model
 
 -- | Determine the equality of two method's pre/post conditions.
 equivalentTo :: LExpr -> LExpr -> IO Response
@@ -34,10 +31,10 @@ equivalentTo lexpr lexpr' = do
 
 -- | Check if two Z3 AST's are equivalent.
 equivalentToZ3 :: Z3 FreeVars -> Z3 AST -> Z3 AST -> IO Response
-equivalentToZ3 freeVars ast1' ast2' =
+equivalentToZ3 fVars ast1' ast2' =
   tryZ3 $ do
     -- Setup
-    fv <- freeVars
+    fv <- fVars
     ast1 <- ast1'
     ast2 <- ast2'
     astEq <- mkEq ast1 ast2
@@ -74,7 +71,7 @@ equivalentToZ3 freeVars ast1' ast2' =
           f <- snd <$> evalAST fv m (k ++ "?length", lenName)
           let len = case f of
                 (IntVal i) -> i
-                _ -> error "non-int length"
+                _          -> error "non-int length"
           -- Iterate array "points"
           modelVals <- forM [0..(len-1)] (\i -> do
             indexAST <- mkInteger $ toInteger i
@@ -87,6 +84,7 @@ equivalentToZ3 freeVars ast1' ast2' =
           return (k, fromString v' :: ModelVal)
 
 -- | Z3 try evaluation with timeout.
+tryZ3 :: Z3 a -> IO a
 tryZ3 = evalZ3With Nothing (  opt "timeout" (5000 :: Integer)
                            +? opt "model_validate" True
                            +? opt "well_sorted_check" True
@@ -95,6 +93,7 @@ tryZ3 = evalZ3With Nothing (  opt "timeout" (5000 :: Integer)
                            )
 
 -- | Sequence tactics.
+(-->) :: String -> String -> Z3 Z3.Tactic
 (-->) t t' = do
   tt <- mkTactic t
   tt' <- mkTactic t'
diff --git a/src/LogicIR/Backend/Z3/Z3.hs b/src/LogicIR/Backend/Z3/Z3.hs
index 6d5ea092e440db2aae13c3f27196b698e12d5e93..f77c05534a6093182af2e7c9236ae944d4313a43 100644
--- a/src/LogicIR/Backend/Z3/Z3.hs
+++ b/src/LogicIR/Backend/Z3/Z3.hs
@@ -1,13 +1,12 @@
 {-# LANGUAGE OverloadedStrings #-}
 module LogicIR.Backend.Z3.Z3 where
 
-import Control.Monad.Trans (liftIO)
 import qualified Data.Map as M
 import Z3.Monad
 
 import LogicIR.Expr
 import LogicIR.Fold
-import LogicIR.Parser
+import LogicIR.Parser ()
 
 lExprToZ3Ast :: LExpr -> Z3 AST
 lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index 9a6c2e91424881e0b1f7541a6f1b3c851546485f..86459355b8d69d6490613104e2a615bb951d95bc 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -1,26 +1,29 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric  #-}
 module LogicIR.Expr where
 
-import Data.String
+import GHC.Generics
+import Control.DeepSeq
 
 -- | The primitive types are bool and int32.
 data Primitive = PBool
                | PInt
                | PReal
-               deriving (Show, Eq, Read)
+               deriving (Show, Eq, Read, Generic, NFData)
 
 -- | A Type can either be a primitive or an array type.
 data Type = TPrim Primitive
           | TArray Type
-          deriving (Show, Eq, Read)
+          deriving (Show, Eq, Read, Generic, NFData)
 
 -- | Typed + named variable.
 data Var = Var Type String
-         deriving (Show, Eq, Read)
+         deriving (Show, Eq, Read, Generic, NFData)
 
 -- | Unary operators.
 data LUnop = NNeg -- -n (numeric negation)
            | LNot -- !n (logical not)
-           deriving (Show, Eq, Read)
+           deriving (Show, Eq, Read, Generic, NFData)
 
 -- | Binary operators.
 data LBinop =
@@ -38,18 +41,18 @@ data LBinop =
             | CEqual -- a == b
             | CLess -- a < b
             | CGreater -- a > b
-            deriving (Show, Eq, Read)
+            deriving (Show, Eq, Read, Generic, NFData)
 
 -- | Quantifier operators.
 data QOp = QAll | QAny
-         deriving (Show, Eq, Read)
+         deriving (Show, Eq, Read, Generic, NFData)
 
 -- | Constants.
 data LConst = CBool Bool
             | CInt Int
             | CReal Double
             | CNil
-            deriving (Show, Eq, Read)
+            deriving (Show, Eq, Read, Generic, NFData)
 
 -- | Logical expressions.
 data LExpr = LConst LConst -- constant
@@ -61,7 +64,7 @@ data LExpr = LConst LConst -- constant
            | LArray Var LExpr -- array access
            | LIsnull Var -- var == null
            | LLen Var -- len(array)
-           deriving (Show, Eq, Read)
+           deriving (Show, Eq, Read, Generic, NFData)
 
 -- Needed for the ArrayModel key ordering in the Map in LogicIR.Backend.ModelGenerator
 instance Ord Var where
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 1706600adc945b7022bc8e87de2e5a7d9f6def36..c50458e84106e8e4eb09cd8f71bce4ed674b5ebd 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -4,15 +4,12 @@ module LogicIR.Frontend.Java (javaExpToLExpr) where
 import Javawlp.Engine.Folds
 import Javawlp.Engine.HelperFunctions
 
-import Language.Java.Parser
 import Language.Java.Pretty
 import Language.Java.Syntax
-import Language.Java.Syntax.Types
 
 import Data.String
-import Data.Typeable
 import LogicIR.Expr
-import LogicIR.Parser
+import LogicIR.Parser ()
 
 javaExpToLExpr :: Exp -> TypeEnv -> [TypeDecl] -> LExpr
 javaExpToLExpr = foldExp javaExpToLExprAlgebra
@@ -89,7 +86,7 @@ javaExpToLExprAlgebra =
                           _ -> error $ "Unimplemented fMethodInv: " ++ show inv
               quantr method name rbegin rend bound expr =
                 let (begin, end) = (refold rbegin, refold rend)
-                    (i, arr) = (Var (TPrim PInt) bound, nameToVar name env decls)
+                    (i, _) = (Var (TPrim PInt) bound, nameToVar name env decls)
                 in case method of
                           "forallr" -> lquantr QAll i begin end expr
                           "existsr" -> lquantr QAny i begin end expr
@@ -99,13 +96,13 @@ javaExpToLExprAlgebra =
               refold expr =
                 foldExp javaExpToLExprAlgebra expr env decls
     fArrayAccess arrayIndex env decls =
-      case arrayIndex of -- TODO: type checking
+      case arrayIndex of
         ArrayIndex (ExpName name) [expr]
           -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
         _
           -> error $ "Multidimensional arrays are not supported: " ++ show arrayIndex
     fExpName name env decls =
-      case name of -- TODO: type checking + check implicit `this.name`
+      case name of
         Name [Ident a, Ident "length"] -> LLen $ nameToVar (Name [Ident a]) env decls
         _ -> LVar $ nameToVar name env decls
     fPostIncrement = error "fPostIncrement has side effects..."
@@ -114,7 +111,7 @@ javaExpToLExprAlgebra =
     fPreDecrement = error "fPreDecrement has side effects..."
     fPrePlus e = e
     fPreMinus e env decls = LUnop NNeg (e env decls)
-    fPreBitCompl e env decls = error "Bitwise operations not supported..."
+    fPreBitCompl _ _ _ = error "Bitwise operations not supported..."
     fPreNot e env decls = LUnop LNot (e env decls)
     fCast = error "fCast is not supported..." -- TODO: perhaps support cast for some types?
     fBinOp e1 op e2 env decls = -- TODO: type checking?
@@ -139,9 +136,9 @@ javaExpToLExprAlgebra =
             GThanE  -> (.>=)
             Equal   -> (.==)
             NotEq   -> (.!=)
-            _ -> error $ "Unsupported operation: " ++ show op
+            _       -> error $ "Unsupported operation: " ++ show op
     fInstanceOf = error "fInstanceOf is not supported..."
-    fCond c a b env decls = LIf (c env decls) (a env decls) (b env decls)
+    fCond c a b_ env decls = LIf (c env decls) (a env decls) (b_ env decls)
     fAssign = error "fAssign has side effects..."
     fLambda = error "fLambda should be handled by fMethodInv..."
     fMethodRef = undefined
diff --git a/src/LogicIR/Pretty.hs b/src/LogicIR/Pretty.hs
index 10df1c7d727b4f37b3288c4fa986c8d474e26837..431b593ab1b64112d566c26f55543bfcb95a9470 100644
--- a/src/LogicIR/Pretty.hs
+++ b/src/LogicIR/Pretty.hs
@@ -1,12 +1,5 @@
--- Very crude pretty printer for debugging, should not be used in production!
 module LogicIR.Pretty (prettyLExpr) where
 
-import Data.List
-import Data.Maybe
-import qualified Data.Map as M
-import Z3.Monad
-import Z3.Opts
-
 import LogicIR.Expr
 import LogicIR.Fold
 
diff --git a/src/Model.hs b/src/Model.hs
index 0757fb57abb4bdfcdbf5ede687cb9129b0ad7efd..59d9658bf46c72f35de672e5b77d870606f85f9e 100644
--- a/src/Model.hs
+++ b/src/Model.hs
@@ -16,10 +16,12 @@ import qualified Text.Parsec.Token as Tokens
 import LogicIR.ParserUtils
 
 -- | Response type.
-data Response = Equivalent | NotEquivalent Model | Undefined | Timeout
+data Response = Equivalent | NotEquivalent Model | ErrorResponse String | Undefined | Timeout
                 deriving (Eq)
 
 (<>) :: Response -> Response -> Response
+ErrorResponse e <> _ = ErrorResponse e
+_ <> ErrorResponse e = ErrorResponse e
 Equivalent <> r = r
 NotEquivalent s <> _ = NotEquivalent s
 Timeout <> _ = Timeout
@@ -27,9 +29,10 @@ Undefined <> _ = Undefined
 
 instance Show Response where
   show Equivalent = "Formulas are equivalent"
+  show (NotEquivalent model) = "Not equivalent: " ++ show model
+  show (ErrorResponse e) = "*** Error: " ++ show e
   show Undefined = "Oops... could not determine if formulas are equivalent"
   show Timeout = "Timeout occured"
-  show (NotEquivalent model) = "Not equivalent: " ++ show model
 
 
 -- | Model type.
diff --git a/src/Server.hs b/src/Server.hs
index 1b436aa1b08ac2849fa89a1c808be283f079f450..6fbb0e39d767abaa9bd5236f46e03b96c9ccef65 100644
--- a/src/Server.hs
+++ b/src/Server.hs
@@ -37,7 +37,6 @@ import Servant.Swagger.UI
 import API (Mode (..), ParseMode (..), compareSpec)
 import Model
 
-
 -- | Data types.
 data ApiReqBody = ApiReqBody
   { sourceA :: String
@@ -46,12 +45,13 @@ data ApiReqBody = ApiReqBody
 instance FromJSON ApiReqBody
 instance ToJSON ApiReqBody
 
-data ApiResponseType = Equiv | NotEquiv | Undef
+data ApiResponseType = Equiv | NotEquiv | Undef | ResponseErr
   deriving (Eq, Show, Generic)
 
 data ApiResponse = ApiResponse
   { responseType :: ApiResponseType
   , model        :: Maybe Model
+  , err          :: Maybe String
   }
   deriving (Eq, Show, Generic)
 instance ToJSON ApiResponseType
@@ -74,10 +74,13 @@ getCompareResponse ApiReqBody {sourceA = srcA, sourceB = srcB} = do
     resp <- liftIO $ compareSpec Release Raw (wrap srcA) (wrap srcB)
     return $ case resp of
                   Equivalent ->
-                    ApiResponse { responseType = Equiv, model = Nothing }
+                    ApiResponse { responseType = Equiv, model = Nothing, err = Nothing }
                   NotEquivalent m ->
-                    ApiResponse { responseType = NotEquiv, model = Just m }
-                  _ -> ApiResponse { responseType = Undef, model = Nothing }
+                    ApiResponse { responseType = NotEquiv, model = Just m, err = Nothing }
+                  ErrorResponse e ->
+                    ApiResponse { responseType = ResponseErr, model = Nothing, err = Just e }
+                  _ ->
+                    ApiResponse { responseType = Undef, model = Nothing, err = Nothing }
     where
       wrap s = ( "public class Main {" ++ s ++ "}"
                , last $ splitOn " " $ head $ splitOn "(" s
@@ -102,6 +105,7 @@ instance ToSample ApiResponse where
       [ ("a", ManyVal [RealVal 0.0, RealVal (-0.5)])
       , ("i", IntVal 10)
       ]
+    , err = Nothing
     }
 
 docsBS :: ByteString
@@ -127,12 +131,10 @@ serverSwagger = swaggerSchemaUIServer (toSwagger (Proxy :: Proxy CompareApi))
 
 -- | Server.
 runApi :: Int -> IO ()
-runApi port = do
-  let settings =
-        setPort port $
-        setBeforeMainLoop (hPutStrLn stderr ("listening on port " ++ show port))
-        defaultSettings
-  runSettings settings app
+runApi port = runSettings settings app
+  where settings = ( setPort port
+                   . setBeforeMainLoop (hPutStrLn stderr ("listening on port " ++ show port))
+                   ) defaultSettings
 
 type WholeApi = CompareApi :<|> SwagApi :<|> Raw
 
diff --git a/z3.log b/z3.log
deleted file mode 100644
index 61b1ef39c713caaf5c6f65cc7640a3dc2e6a1882..0000000000000000000000000000000000000000
Binary files a/z3.log and /dev/null differ