diff --git a/.gitignore b/.gitignore
index 56788422c61a0fbd6d3eca2313e194da50b96b41..35ad64dcc799fc91e532d9b3970e618b86a47889 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,5 @@ tests/org/
 *.hi
 *.o
 .DS_Store
+/src/ModelParser/Lexer.hs
+/src/ModelParser/Parser.hs
diff --git a/src/ModelParser/Model.hs b/src/ModelParser/Model.hs
new file mode 100644
index 0000000000000000000000000000000000000000..0e5cfd05fc18b1c7f4c662388bf21f6a997a4d96
--- /dev/null
+++ b/src/ModelParser/Model.hs
@@ -0,0 +1,14 @@
+module ModelParser.Model where
+
+data FuncInst = InstInt Int Int
+              | InstElse Int
+              deriving (Show, Read, Eq)
+
+data ModelVal = BoolVal Bool
+              | IntVal Int
+              | ArrayRef String -- TODO: immediately forward to ArrayFunc?
+              | ArrayAsConst Int -- TODO: parse to InstElse?
+              | ArrayFunc [FuncInst]
+              deriving (Show, Read, Eq)
+
+type Z3Model = [(String, ModelVal)]
\ No newline at end of file
diff --git a/src/ModelParser/Parser.y b/src/ModelParser/Parser.y
index 20b05a76a8cd291e8ee3a29f857949080234e89b..c9b15762aa92cf7f49eb1e81867823fce4cbe254 100644
--- a/src/ModelParser/Parser.y
+++ b/src/ModelParser/Parser.y
@@ -1,7 +1,8 @@
 {
-module ModelParser.Parser where
+module ModelParser.Parser (parseModel) where
 
 import ModelParser.Lexer
+import ModelParser.Model
 }
 
 %name happyParseTokens
@@ -46,22 +47,11 @@ FuncEntry : value "->" value { InstInt $1 $3 }
           | value { InstElse $1 }
 
 {
-data FuncInst = InstInt Int Int
-              | InstElse Int
-              deriving (Show, Read, Eq)
-
-data ModelVal = BoolVal Bool
-              | IntVal Int
-              | ArrayRef String -- TODO: immediately forward to ArrayFunc?
-              | ArrayAsConst Int -- TODO: parse to InstElse?
-              | ArrayFunc [FuncInst]
-              deriving (Show, Read, Eq)
-
-type Z3Model = [(String, ModelVal)]
 
 parseError :: [Token] -> a
-parseError t = error $ "Parse error" ++ show t
+parseError t = error $ "Model parse error " ++ show t
 
 parseModel :: String -> Z3Model
 parseModel = happyParseTokens . alexScanTokens
+
 }
\ No newline at end of file
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 778ddef9692e24f6674b03ab3b1568236dbb4145..fae4e58da20d72ad63de71d310df96f73bc6685e 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -18,6 +18,7 @@ import LogicIR.Backend.Pretty
 import LogicIR.Backend.Null
 
 import ModelParser.Parser
+import ModelParser.Model
 
 import Control.Monad.Trans (liftIO)