diff --git a/javawlp.cabal b/javawlp.cabal
index 9d5d22666a6dc4fa164364bbdaa54950ee9d0cb7..f00c9ed1c00c518abbffc8dd5ac9e77f86283451 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -28,6 +28,7 @@ library
                      , LogicIR.Pretty
                      , LogicIR.Frontend.Java
                      , LogicIR.Eval
+                     , LogicIR.ParserUtils
                      -- Checker
                      , SimpleFormulaChecker
                      -- Z3
diff --git a/src/LogicIR/Backend/Z3/API.hs b/src/LogicIR/Backend/Z3/API.hs
index f26f9786b1a1741a3529d798a7462928e64bfe38..4bbe333985cfd136ae721c18600b34c4eeda583b 100644
--- a/src/LogicIR/Backend/Z3/API.hs
+++ b/src/LogicIR/Backend/Z3/API.hs
@@ -23,9 +23,6 @@ equivalentTo :: LExpr -> LExpr -> IO Z3Response
 equivalentTo lexpr lexpr' = do
     let fv = freeVars2 lexpr lexpr'
     let (ast, ast') = (lExprToZ3Ast lexpr, lExprToZ3Ast lexpr')
-    asts <- showZ3AST ast
-    asts' <- showZ3AST ast'
-    -- putStrLn $ "Z3_AST1:\n" ++ asts ++ "\n\nZ3_AST2:\n" ++ asts' ++ "\n"
     res <- tryJust errorSelector $ equivalentToZ3 fv ast ast'
     case res of
       Left () -> return Timeout
@@ -37,18 +34,12 @@ equivalentTo lexpr lexpr' = do
           InvalidUsage -> Just ()
           _            -> Nothing
 
--- | Sequence tactics.
-(-->) t t' = do
-  tt <- mkTactic t
-  tt' <- mkTactic t'
-  andThenTactic tt tt'
-
 -- | Check if two Z3 AST's are equivalent.
 equivalentToZ3 :: Z3 FreeVars -> Z3 AST -> Z3 AST -> IO Z3Response
 equivalentToZ3 freeVars ast1' ast2' =
   tryZ3 $ do
+    -- Setup
     fv <- freeVars
-    -- liftIO $ putStr "FreeVars: " >> print (M.keys fv)
     ast1 <- ast1'
     ast2 <- ast2'
     astEq <- mkEq ast1 ast2
@@ -60,46 +51,43 @@ equivalentToZ3 freeVars ast1' ast2' =
     t <- "qe" --> "aig"
     a <- applyTactic t g
     asts <- getGoalFormulas =<< getApplyResultSubgoal a 0
-    -- liftIO $ putStrLn "After tactics:"
-    -- astStrs <- mapM astToString asts
-    -- forM_ astStrs (liftIO . putStrLn)
     g' <- mkAnd asts
     assert g'
 
-    -- assert astNeq
-    (r, model) <- solverCheckAndGetModel -- check in documentation
+    -- Get model
+    (r, model) <- solverCheckAndGetModel
 
-    case r of
+    response <- case r of
       Unsat -> return Equivalent
       Undef -> return Undefined
       Sat   -> do
-        let m = fromJust model
-        ms <- M.fromList <$> forM (M.toList fv) (evalAST fv m)
-        let ms' = sanitize ms
-        liftIO $ putStr "Model: " >> print ms'
-        return $ NotEquivalent ms'
-    -- solverReset
-    where evalAST :: FreeVars -> Model -> (String, AST) -> Z3 (String, ModelVal)
-          evalAST fv m (k, ast) = do
-            v <- fromJust <$> modelEval m ast True
-            sortKind <- getSort v >>= getSortKind
-            if sortKind == Z3_ARRAY_SORT then do
-              -- Retrieve array's length
-              lenName <- mkStringSymbol (k ++ "?length") >>= mkIntVar
-              f <- snd <$> evalAST fv m (k ++ "?length", lenName)
-              let len = case f of
-                    (IntVal i) -> i
-                    _ -> error "non-int length"
-              -- Iterate array "points"
-              modelVals <- forM [0..(len-1)] (\i -> do
-                indexAST <- mkInteger $ toInteger i
-                pointAST <- mkSelect v indexAST
-                snd <$> evalAST fv m ("", pointAST)
-                )
-              return (k, ManyVal modelVals)
-            else do
-              v' <- astToString v
-              return (k, fromString v' :: ModelVal)
+        ms <- M.fromList <$> forM (M.toList fv) (evalAST fv (fromJust model))
+        return $ NotEquivalent (sanitize ms)
+    solverReset
+    return response
+    where
+      -- Construct model values
+      evalAST :: FreeVars -> Model -> (String, AST) -> Z3 (String, ModelVal)
+      evalAST fv m (k, ast) = do
+        v <- fromJust <$> modelEval m ast True
+        sortKind <- getSort v >>= getSortKind
+        if sortKind == Z3_ARRAY_SORT then do
+          -- Retrieve array's length
+          lenName <- mkStringSymbol (k ++ "?length") >>= mkIntVar
+          f <- snd <$> evalAST fv m (k ++ "?length", lenName)
+          let len = case f of
+                (IntVal i) -> i
+                _ -> error "non-int length"
+          -- Iterate array "points"
+          modelVals <- forM [0..(len-1)] (\i -> do
+            indexAST <- mkInteger $ toInteger i
+            pointAST <- mkSelect v indexAST
+            snd <$> evalAST fv m ("", pointAST)
+            )
+          return (k, ManyVal modelVals)
+        else do
+          v' <- astToString v
+          return (k, fromString v' :: ModelVal)
 
 -- | Z3 try evaluation with timeout.
 tryZ3 = evalZ3With Nothing (  opt "timeout" (5000 :: Integer)
@@ -108,6 +96,12 @@ tryZ3 = evalZ3With Nothing (  opt "timeout" (5000 :: Integer)
                            +? opt "auto_config" True
                            -- +? opt "unsat_core" True
                            )
+                           
+-- | Sequence tactics.
+(-->) t t' = do
+  tt <- mkTactic t
+  tt' <- mkTactic t'
+  andThenTactic tt tt'
 
 -- | Pretty-print Z3 AST.
 showZ3AST :: Z3 AST -> IO String
diff --git a/src/LogicIR/Backend/Z3/Model.hs b/src/LogicIR/Backend/Z3/Model.hs
index 943585f4296a71bf9a58e88771bb6d1c77a20491..5d6e894879be5b92ca5dc6f2f01531365b5041fc 100644
--- a/src/LogicIR/Backend/Z3/Model.hs
+++ b/src/LogicIR/Backend/Z3/Model.hs
@@ -1,17 +1,17 @@
-{-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE OverloadedStrings #-}
 module LogicIR.Backend.Z3.Model where
 
 import qualified Data.Map as M
-
 import Data.String
 import Text.Parsec hiding (runP)
-import Text.Parsec.Char
 import Text.Parsec.Expr
 import Text.Parsec.Language
 import Text.Parsec.String
 import qualified Text.Parsec.Token as Tokens
 
+import LogicIR.ParserUtils
+
+-- | Data type.
 data ModelVal = BoolVal Bool
               | IntVal Integer
               | RealVal Double
@@ -21,6 +21,7 @@ data ModelVal = BoolVal Bool
 type Z3Model = M.Map String ModelVal
 emptyZ3Model = M.empty :: Z3Model
 
+-- | Pretty-printing.
 instance Show ModelVal where
   show (BoolVal b)  = show b
   show (IntVal i)   = show i
@@ -37,17 +38,7 @@ sanitize model = M.mapWithKey f model
             (IntVal i) -> i
             _ -> error "non-int length"
 
--- | Implicit conversion from strings.
-instance IsString ModelVal where
-  fromString = runP modelP
-
--- | Parser.
-runP :: Parser a -> String -> a
-runP p s =
-  case runParser (p <* eof) () "" s of
-        Left err -> error $ show err
-        Right r  -> r
-
+-- | Parsers.
 modelP :: Parser ModelVal
 modelP = try (BoolVal <$> boolP)
      <|> try (RealVal <$> realP)
@@ -74,14 +65,6 @@ indexP = Tokens.natural haskell
 boolP :: Parser Bool
 boolP = (True <$ str "true") <|> (False <$ str "false")
 
--- | Useful marcros.
-lexeme p = spaces *> p <* spaces
-str = lexeme . string
-commas l = l `sepBy` string ", "
-(<~) p s = p <* lexeme (string s)
-(~>) s p = lexeme (string s) *> p
-parens = Tokens.parens haskell
-reserved = Tokens.reservedOp haskell
-infix_ op f = Infix (reserved op >> return f) AssocLeft
-prefix op f = Prefix (reserved op >> return f)
-postfix op f = Postfix (reserved op >> return f)
+-- | Implicit conversion from strings.
+instance IsString ModelVal where
+  fromString = runP modelP
diff --git a/src/LogicIR/Null.hs b/src/LogicIR/Null.hs
index 50531dfd73fa0df2be575b4723b19d8c6649963a..5a1919b112ebe9cf02299afa68b57728e828b351 100644
--- a/src/LogicIR/Null.hs
+++ b/src/LogicIR/Null.hs
@@ -1,7 +1,7 @@
 module LogicIR.Null (lExprPreprocessNull) where
 
-import           LogicIR.Expr
-import           LogicIR.Fold
+import LogicIR.Expr
+import LogicIR.Fold
 
 -- | Replace all instances of "a ==/!= null" with (!)isNull(a).
 lExprPreprocessNull :: LExpr -> LExpr
diff --git a/src/LogicIR/Parser.hs b/src/LogicIR/Parser.hs
index b14b9cf9a10334762147103637c67a42ba95d0cf..85424327cceda36f98981ce0b27319e7a5d7f6ea 100644
--- a/src/LogicIR/Parser.hs
+++ b/src/LogicIR/Parser.hs
@@ -1,25 +1,16 @@
-{-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE OverloadedStrings #-}
 module LogicIR.Parser where
 
 import Data.String
-import System.IO.Unsafe (unsafePerformIO)
 import Text.Parsec hiding (runP)
-import Text.Parsec.Char
 import Text.Parsec.Expr
 import Text.Parsec.Language
 import Text.Parsec.String
 import qualified Text.Parsec.Token as Tokens
 
+import LogicIR.ParserUtils
 import LogicIR.Expr
 
--- | Run parser.
-runP :: Parser a -> String -> a
-runP p s = unsafePerformIO $
-  case runParser (p <* eof) () "" s of
-        Left err   -> fail $ show err
-        Right lExp -> return lExp
-
 -- | Parser for logical expressions.
 exprP :: Parser LExpr
 exprP =
@@ -99,19 +90,6 @@ typeP = try (TPrim <$> primTypeP) <|> (TArray <$> arrayTypeP)
                    <|> (PReal <$ str "real")
     arrayTypeP = "[" ~> typeP <~ "]"
 
--- | Useful marcros.
-lexeme p = spaces *> p <* spaces
-str = lexeme . string
-commas l = l `sepBy` string ", "
-(<~) p s = p <* lexeme (string s)
-(~>) s p = lexeme (string s) *> p
-parens = Tokens.parens haskell
-identifier = Tokens.identifier haskell
-reserved = Tokens.reservedOp haskell
-infix_ op f = Infix (reserved op >> return f) AssocLeft
-prefix op f = Prefix (reserved op >> return f)
-postfix op f = Postfix (reserved op >> return f)
-
 -- | Implicit conversions from strings.
 instance IsString LExpr where
   fromString = runP exprP
diff --git a/src/LogicIR/ParserUtils.hs b/src/LogicIR/ParserUtils.hs
new file mode 100644
index 0000000000000000000000000000000000000000..25a247a6b62ff2ee46a83f3953da006f4fbdbc04
--- /dev/null
+++ b/src/LogicIR/ParserUtils.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE FlexibleContexts  #-}
+module LogicIR.ParserUtils where
+
+import Text.Parsec
+import Text.Parsec.Expr
+import Text.Parsec.Language
+import Text.Parsec.String
+import qualified Text.Parsec.Token as Tokens
+
+-- | Run parser.
+runP :: Parser a -> String -> a
+runP p s =
+  case runParser (p <* eof) () "" s of
+        Left err   -> error $ show err
+        Right x -> x
+
+-- | Useful marcros.
+lexeme p = spaces *> p <* spaces
+str = lexeme . string :: String -> Parser String
+commas l = l `sepBy` string ", "
+(<~) p s = p <* lexeme (string s)
+(~>) s p = lexeme (string s) *> p
+parens = Tokens.parens haskell
+identifier = Tokens.identifier haskell
+reserved = Tokens.reservedOp haskell
+infix_ op f = Infix (reserved op >> return f) AssocLeft
+prefix op f = Prefix (reserved op >> return f)
+postfix op f = Postfix (reserved op >> return f)