diff --git a/g2.cabal b/g2.cabal
--- a/g2.cabal
+++ b/g2.cabal
@@ -2,7 +2,7 @@
 -- see http://haskell.org/cabal/users-guide/
 
 name:                g2
-version:             0.1.0.0
+version:             0.1.0.1
 synopsis:            Haskell symbolic execution engine.
 description:         A Haskell symbolic execution engine.
                      
@@ -193,7 +193,6 @@
   main-is:             Main.hs
 
 executable QuasiQuote
-  -- other-modules:   
   -- other-extensions:    
   build-depends:         g2
                        , base >= 4.8 && < 5
@@ -204,6 +203,17 @@
                        -- -fprof-auto "-with-rtsopts=-p"
   hs-source-dirs:      quasiquote
   main-is:             Main.hs
+  other-modules:         Arithmetics.Interpreter
+                       , Arithmetics.Test
+                       , DeBruijn.Interpreter
+                       , DeBruijn.Test
+                       , Evaluations
+                       , Lambda.Interpreter
+                       , Lambda.Test
+                       , NQueens.Encoding
+                       , NQueens.Test
+                       , RegEx.RegEx
+                       , RegEx.Test
 
 test-suite test
   build-depends:         g2
@@ -223,6 +233,16 @@
   default-language:    Haskell2010
   hs-source-dirs:      tests
   main-is:             Test.hs
+  other-modules:         CaseTest
+                       , DefuncTest
+                       , Expr
+                       , GetNthTest
+                       , HigherOrderMathTest
+                       , InputOutputTest
+                       , PeanoTest
+                       , Reqs
+                       , TestUtils
+                       , Typing
   ghc-options:         -Wall
                        -- -fprof-auto "-with-rtsopts=-p"
                        -threaded
diff --git a/quasiquote/Arithmetics/Interpreter.hs b/quasiquote/Arithmetics/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/Arithmetics/Interpreter.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Arithmetics.Interpreter where
+
+import Control.Monad
+import Data.Data
+import G2.QuasiQuotes.G2Rep
+
+type Ident = String
+type Env = [(Ident, Int)]
+
+data AExpr = I Int | Var Ident
+    | Add AExpr AExpr | Mul AExpr AExpr
+    deriving (Eq, Show, Data)
+
+$(derivingG2Rep ''AExpr)
+
+data BExpr = Not BExpr | And BExpr BExpr | Or BExpr BExpr
+    | Lt AExpr AExpr | Eq AExpr AExpr
+    deriving (Eq, Show, Data)
+
+$(derivingG2Rep ''BExpr)
+
+type Stmts = [Stmt]
+data Stmt = Assign Ident AExpr
+          | If BExpr Stmts Stmts
+          | While BExpr Stmts
+          | Assert BExpr
+          deriving (Eq, Show, Data)
+          
+$(derivingG2Rep ''Stmt)
+
+type Bound = [Ident]
+type Return = Ident
+data Func = Func Bound Stmts Return
+
+$(derivingG2Rep ''Func)
+
+evalFunc :: [Int] -> Func -> Maybe Int
+evalFunc is (Func b s r) =
+  lookup r =<< evalStmts (zip b is) s
+
+evalStmts :: Env -> Stmts -> Maybe Env
+evalStmts = foldM evalStmt  
+
+evalStmt :: Env -> Stmt -> Maybe Env
+evalStmt env (Assign ident aexpr) =
+  Just $ (ident, evalA env aexpr):env
+evalStmt env (If bexpr lhs rhs) =
+  if evalB env bexpr
+    then evalStmts env lhs
+    else evalStmts env rhs
+evalStmt env (While bexpr loop) =
+  if evalB env bexpr
+    then evalStmts env (loop ++ [While bexpr loop])
+    else Just env
+evalStmt env (Assert bexpr) =
+  if evalB env bexpr
+    then Just env
+    else Nothing
+
+evalA :: Env -> AExpr -> Int
+evalA _ (I int) = int
+evalA env (Add lhs rhs) =
+  evalA env lhs + evalA env rhs
+evalA env (Mul lhs rhs) =
+  evalA env lhs * evalA env rhs
+evalA env (Var ident) =
+  case lookup ident env of
+    Just int -> int
+    _ -> error $
+          "lookup with " ++ show (ident, env)
+
+evalB :: Env -> BExpr -> Bool
+evalB env (Not bexpr) = not $ evalB env bexpr
+evalB env (And lhs rhs) =
+  evalB env lhs && evalB env rhs
+evalB env (Or lhs rhs) =
+  evalB env lhs || evalB env rhs
+evalB env (Lt lhs rhs) =
+  evalA env lhs < evalA env rhs
+evalB env (Eq lhs rhs) =
+  evalA env lhs == evalA env rhs
+
diff --git a/quasiquote/Arithmetics/Test.hs b/quasiquote/Arithmetics/Test.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/Arithmetics/Test.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Arithmetics.Test where
+
+import Arithmetics.Interpreter
+import G2.QuasiQuotes.QuasiQuotes
+
+productTest :: IO (Maybe (AExpr, AExpr))
+productTest =
+  [g2| \(a :: Int) -> ?(s1 :: AExpr)
+                      ?(s2 :: AExpr) |
+    let env = [("x", 23), ("y", 59)] in
+    let lhs = Mul (Var "x") (Var "y") in
+    let rhs = Mul s1 s2 in
+      evalB env (Eq lhs rhs) |] 0
+
+envTest :: BExpr -> IO (Maybe Env)
+envTest = [g2|\(b :: BExpr) -> ?(env :: Env) |
+                evalB env b |]
+
+assertViolation :: Stmts -> IO (Maybe Env)
+assertViolation = [g2|\(stmts :: Stmts) -> ?(env :: Env) |
+                       evalStmts env stmts == Nothing|]
+
+productSumTest :: IO (Maybe Env)
+productSumTest =
+    envTest $ And
+                ((Eq 
+                    (Mul (Var "x") (Var "y"))
+                    (Add (Var "x") (Var "y"))))
+                (Lt (I 0) (Var "x"))
+
+
+assertViolationTest1 :: IO (Maybe Env)
+assertViolationTest1 = assertViolation
+  [ Assert (Lt (I 5) (I 3)) ]
+
+-- x^2 + y^2 + z^2 < (x + y + z)^2
+assertViolationTest2 :: IO (Maybe Env)
+assertViolationTest2 = assertViolation
+  [ Assign "v1" (Add (Var "x") (Add (Var "y") (Var "z")))
+  , Assign "v1" (Mul (Var "v1") (Var "v1"))
+  , Assign "v2" (Add (Mul (Var "x") (Var "x"))
+                  (Add (Mul (Var "y") (Var "y"))
+                       (Mul (Var "z") (Var "z"))))
+  , Assert (Lt (Var "v2") (Var "v1"))
+  ]
+
+
+assertViolationTest3 :: IO (Maybe Env)
+assertViolationTest3 = assertViolation
+  [
+    Assign "k" (I 1),
+    Assign "i" (I 0),
+    Assign "j" (I 0),
+    Assign "n" (I 5),
+    While (Or (Lt (Var "i") (Var "n"))
+              (Eq (Var "i") (Var "n")))
+          [ Assign "i" (Add (Var "i") (I 1))
+          , Assign "j" (Add (Var "j") (Var "i"))
+          ],
+    Assign "z" (Add (Var "k") (Add (Var "i") (Var "j"))),
+    Assert (Lt (Mul (Var "n") (I 2)) (Var "z"))
+  ]
+  
+
+assertViolationTest4 :: IO (Maybe Env)
+assertViolationTest4 = assertViolation
+  [
+    Assign "k" (I 1),
+    Assign "i" (I 0),
+    -- Assign "j" (I 0),
+    Assign "n" (I 5),
+    While (Or (Lt (Var "i") (Var "n"))
+              (Eq (Var "i") (Var "n")))
+          [ Assign "i" (Add (Var "i") (I 1))
+          , Assign "j" (Add (Var "j") (Var "i"))
+          ],
+    Assign "z" (Add (Var "k") (Add (Var "i") (Var "j"))),
+    Assert (Lt (Mul (Var "n") (I 2)) (Var "z"))
+  ]
+ 
+
diff --git a/quasiquote/DeBruijn/Interpreter.hs b/quasiquote/DeBruijn/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/DeBruijn/Interpreter.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module DeBruijn.Interpreter ( Expr (..)
+                            , Ident
+                            , eval
+                            , app
+                            , lams
+                            , num) where
+
+import Data.Data
+import G2.QuasiQuotes.G2Rep
+
+type Ident = Int
+
+data Expr = Var Ident
+          | Lam Expr
+          | App Expr Expr
+          deriving (Show, Read, Eq, Data)
+
+$(derivingG2Rep ''Expr)
+
+type Stack = [Expr]
+
+eval :: Expr -> Expr
+eval = eval' []
+
+eval' :: Stack -> Expr -> Expr
+eval' (e:stck) (Lam e') = eval' stck (rep 1 e e')
+eval' stck (App e1 e2) = eval' (e2:stck) e1
+eval' stck e = app $ e:stck
+
+rep :: Int -> Expr -> Expr -> Expr
+rep i e v@(Var j)
+    | i == j = e
+    | otherwise = v
+rep i e (Lam e') = Lam (rep (i + 1) e e')
+rep i e (App e1 e2) = App (rep i e e1) (rep i e e2)
+
+app :: [Expr] -> Expr
+app = foldl1 App
+
+lams :: Int -> Expr -> Expr
+lams n e = iterate Lam e !! n
+
+num :: Int -> Expr
+num n = Lam $ Lam $ foldr1 App (replicate n (Var 2) ++ [Var 1])
diff --git a/quasiquote/DeBruijn/Test.hs b/quasiquote/DeBruijn/Test.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/DeBruijn/Test.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module DeBruijn.Test where
+
+import DeBruijn.Interpreter
+import G2.QuasiQuotes.QuasiQuotes
+
+solveDeBruijn1 :: IO (Maybe Expr)
+solveDeBruijn1 =
+    [g2| \(x :: Int) -> ?(syExpr :: Expr) |
+        let expr = App syExpr in
+          eval (expr (Lam (Var 1))) == (Lam (Var 1))
+        && eval (expr (Lam (Var 2))) == (Lam (Var 2)) |] 6
+
+solveDeBruijn :: [([Expr], Expr)] -> IO (Maybe Expr)
+solveDeBruijn =
+    [g2| \(es :: [([Expr], Expr)]) -> ?(func :: Expr) |
+         all (\e -> (eval (app (func:fst e))) == snd e) es |]
+
+solveDeBruijnI :: IO (Maybe Expr)
+solveDeBruijnI = solveDeBruijn [ ([num 1], num 1)
+                               , ([num 2], num 2) ]
+
+solveDeBruijnK :: IO (Maybe Expr)
+solveDeBruijnK = solveDeBruijn [ ([num 1, num 2], num 2)
+                               , ([num 2, num 3], num 3)]
+
+trueLam :: Expr
+trueLam = Lam (Lam (Var 2))
+
+falseLam :: Expr
+falseLam = Lam (Lam (Var 1))
+
+solveDeBruijnAnd :: IO (Maybe Expr)
+solveDeBruijnAnd = solveDeBruijn [ ([trueLam, trueLam], trueLam)
+                                 , ([falseLam, falseLam], falseLam)
+                                 , ([falseLam, trueLam], falseLam) 
+                                 , ([trueLam, falseLam], falseLam) ]
+
+solveDeBruijnOr :: IO (Maybe Expr)
+solveDeBruijnOr = solveDeBruijn [ ([trueLam, trueLam], trueLam)
+                                  , ([falseLam, falseLam], falseLam)
+                                  , ([falseLam, trueLam], trueLam) 
+                                  , ([trueLam, falseLam], trueLam) ]
+
+solveDeBruijnIte :: IO (Maybe Expr)
+solveDeBruijnIte = solveDeBruijn [ ([trueLam, Var 2, Var 4], Var 2)
+                                 , ([falseLam, Var 2, Var 4], Var 4) ]
+
+solveDeBruijnS :: IO (Maybe Expr)
+solveDeBruijnS =
+    solveDeBruijn
+        [ ([Lam (Lam (Var 1)), Lam (Var 1), num 2], num 2)
+        , ([Lam (Lam (Var 1)), Lam (Lam (Var 2)), num 3], num 3) ]
+    -- [g2| \(_ :: ()) -> ?(func :: Expr) |
+    --     let
+    --         k = Lam (Lam (Var 2))
+    --     in
+    --     eval (App func (App k (App (num 1) (num 2)))) == num 2
+    -- |] ()
+    -- , ([Lam (Lam (Var 1)), Lam (num 3), num 1], num 3)]
+    -- , ([Lam (Lam (Lam (Var 2))), Lam (Lam (Var 1)), num 1], Lam (Lam (num 1)))]
diff --git a/quasiquote/Evaluations.hs b/quasiquote/Evaluations.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/Evaluations.hs
@@ -0,0 +1,194 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Evaluations where
+
+import Data.Time.Clock
+import G2.QuasiQuotes.QuasiQuotes
+
+import Arithmetics.Interpreter as A
+import DeBruijn.Interpreter as D
+import RegEx.RegEx as R
+
+
+timeIOAction :: IO a -> IO (a, NominalDiffTime)
+timeIOAction action = do
+  start <- getCurrentTime
+  res <- action
+  end <- getCurrentTime
+  let diff = diffUTCTime end start
+  return (res, diff)
+
+timeIOActionPrint :: Show a => IO a -> IO ()
+timeIOActionPrint action = do
+  (res, time) <- timeIOAction action
+  putStrLn $ show res
+  putStrLn $ "time: " ++ show time
+
+
+-------------------------------------------
+-------------------------------------------
+-- Section 2 (Arithmetics)
+searchBadEnv :: Stmts -> IO (Maybe Env)
+searchBadEnv =
+  [g2| \(stmts :: Stmts) -> ?(env :: Env) |
+        evalStmts env stmts == Nothing|]
+
+envTest :: BExpr -> IO (Maybe Env)
+envTest = [g2|\(b :: BExpr) -> ?(env :: Env) |
+                evalB env b |]
+
+badProg :: Stmts
+badProg =
+  [
+    Assign "k" (I 1),
+    Assign "i" (I 0),
+    -- Assign "j" (I 0),
+    Assign "n" (I 5),
+    While (A.Or (Lt (A.Var "i") (A.Var "n"))
+              (Eq (A.Var "i") (A.Var "n")))
+          [ Assign "i" (Add (A.Var "i") (I 1))
+          , Assign "j" (Add (A.Var "j") (A.Var "i"))
+          ],
+    Assign "z" (Add (A.Var "k") (Add (A.Var "i") (A.Var "j"))),
+    Assert (Lt (Mul (A.Var "n") (I 2)) (A.Var "z"))
+  ]
+
+productSumTest :: BExpr
+productSumTest =
+  And
+    ((Eq 
+      (Mul (A.Var "x") (A.Var "y"))
+      (Add (A.Var "x") (A.Var "y"))))
+    (Lt (I 0) (A.Var "x"))
+
+runArithmeticsEval :: IO ()
+runArithmeticsEval = do
+  putStrLn "------------------------"
+  putStrLn "-- Arithmetics Eval -------"
+  timeIOActionPrint $ searchBadEnv badProg
+  timeIOActionPrint $ envTest productSumTest
+  putStrLn ""
+
+
+
+-------------------------------------------
+-------------------------------------------
+-- Section 5.1 (n Queens)
+
+
+-------------------------------------------
+-------------------------------------------
+-- Section 5.2 (Lambda Calculus)
+
+solveDeBruijn :: [([Expr], Expr)] -> IO (Maybe Expr)
+solveDeBruijn =
+    [g2| \(es :: [([Expr], Expr)]) -> ?(func :: Expr) |
+         all (\e -> (eval (app (func:fst e))) == snd e) es |]
+
+idDeBruijn :: [([D.Expr], D.Expr)]
+idDeBruijn = [ ([num 1], num 1)
+             , ([num 2], num 2) ]
+
+const2Example :: [([D.Expr], D.Expr)]
+const2Example =
+  [ ([num 1, num 2], num 1)
+  , ([num 2, num 3], num 2) ]                
+
+trueLam :: D.Expr
+trueLam = Lam (Lam (D.Var 2))
+
+falseLam :: D.Expr
+falseLam = Lam (Lam (D.Var 1))
+
+notExample :: [([D.Expr], D.Expr)]
+notExample =
+  [ ([trueLam], falseLam)
+  , ([falseLam], trueLam) ]
+
+orExample :: [([D.Expr], D.Expr)]
+orExample =
+  [ ([trueLam, trueLam], trueLam)
+  , ([falseLam, falseLam], falseLam)
+  , ([falseLam, trueLam], trueLam)
+  , ([trueLam, falseLam], trueLam )]
+
+andExample :: [([D.Expr], D.Expr)]
+andExample =
+  [ ([trueLam, trueLam], trueLam)
+  , ([falseLam, falseLam], falseLam)
+  , ([falseLam, trueLam], falseLam)
+  , ([trueLam, falseLam], falseLam )]
+
+
+runDeBruijnEval :: IO ()
+runDeBruijnEval = do
+  putStrLn "------------------------"
+  putStrLn "-- DeBruijn Eval -------"
+  timeIOActionPrint $ solveDeBruijn idDeBruijn
+  timeIOActionPrint $ solveDeBruijn const2Example
+  -- timeIOActionPrint $ solveDeBruijn notExample
+  timeIOActionPrint $ solveDeBruijn orExample
+  -- timeIOActionPrint $ solveDeBruijn andExample
+  putStrLn ""
+
+
+-------------------------------------------
+-------------------------------------------
+-- Section 5.3 (Regular Expressions)
+
+stringSearch :: RegEx -> IO (Maybe String)
+stringSearch =
+  [g2| \(r :: RegEx) -> ?(str :: String) |
+        match r str |]
+
+-- (a + b)* c (d + (e f)*)
+regex1 :: RegEx
+regex1 =
+  Concat (Star (R.Or (Atom 'a') (Atom 'b')))
+         (Concat (Atom 'c')
+                 (R.Or (Atom 'd')
+                     (Concat (Atom 'e')
+                             (Atom 'f'))))
+
+regex2 :: RegEx
+regex2 = Concat (Atom 'a')
+         (Concat (Atom 'b')
+         (Concat (Atom 'c')
+         (Concat (Atom 'd')
+         (Concat (Atom 'e')
+         ((Atom 'f'))))))
+
+regex3 :: RegEx
+regex3 = R.Or (Atom 'a')
+         (R.Or (Atom 'b')
+         (R.Or (Atom 'c')
+         (R.Or (Atom 'd')
+         (R.Or (Atom 'e')
+         ((Atom 'f'))))))
+
+regex4 :: RegEx
+regex4 = Concat (Star (Atom 'a'))
+          (Concat (Star (Atom 'b'))
+          (Concat (Star (Atom 'c'))
+          (Concat (Star (Atom 'd'))
+          (Concat (Star (Atom 'e'))
+          ((Star (Atom 'f')))))))
+
+
+
+runRegExEval :: IO ()
+runRegExEval = do
+  putStrLn "------------------------"
+  putStrLn "-- RegEx Eval ----------"
+  timeIOActionPrint $ stringSearch regex1
+  timeIOActionPrint $ stringSearch regex2
+  timeIOActionPrint $ stringSearch regex3
+  timeIOActionPrint $ stringSearch regex4
+  putStrLn ""
+
+
+
+-------------------------------------------
+-------------------------------------------
+
+
diff --git a/quasiquote/Lambda/Interpreter.hs b/quasiquote/Lambda/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/Lambda/Interpreter.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Lambda.Interpreter where
+
+import Data.Data
+import Data.List
+import G2.QuasiQuotes.QuasiQuotes
+import G2.QuasiQuotes.G2Rep
+
+type Id = String
+
+data Prim = I Int | B Bool | Fun Id
+  deriving (Show, Eq, Data)
+
+$(derivingG2Rep ''Prim)
+
+data Expr
+  = Var Id
+  | Lam Id Expr
+  | App Expr Expr
+  | Const Prim
+  deriving (Show, Eq, Data)
+
+$(derivingG2Rep ''Expr)
+
+type Env = [(Id, Expr)]
+
+eval :: Env -> Expr -> Expr
+eval env (Var id) =
+  case lookup id env of
+    Just expr -> eval env expr
+    Nothing -> Const (Fun id)
+eval env (App (Lam i body) arg) =
+  eval ((i, arg) : env) body
+eval env expr = expr
+
diff --git a/quasiquote/Lambda/Test.hs b/quasiquote/Lambda/Test.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/Lambda/Test.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Lambda.Test where
+
+import Lambda.Interpreter
+import G2.QuasiQuotes.QuasiQuotes
+
+lambdaTest1 :: IO (Maybe Expr)
+lambdaTest1 = [g2| \(x :: Int ) -> ?(symExpr :: Expr) |
+      let env = [] in
+      let expr = App (Lam "b" (Var "b")) symExpr in
+        eval env expr == (Const (I 40)) |] 0
+
+
+lambdaTest2 :: IO (Maybe Expr)
+lambdaTest2 = [g2| \(x :: Int ) -> ?(symExpr :: Expr) |
+      let env = [] in
+      let expr = symExpr in
+        eval env expr == (Const (I 43)) |] 0
diff --git a/quasiquote/NQueens/Encoding.hs b/quasiquote/NQueens/Encoding.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/NQueens/Encoding.hs
@@ -0,0 +1,62 @@
+module NQueens.Encoding where
+
+import Data.List
+
+type Queen = Int
+
+indexPairs :: Int -> [(Int,Int)]
+indexPairs n = [(i, j) | i <- [0..n-1], j <- [i+1..n-1]]
+
+legal :: Int -> Queen -> Bool
+legal n qs = 1 <= qs && qs <= n
+
+queenPairSafe :: Int -> [Queen] -> (Int, Int) -> Bool
+queenPairSafe n qs (i, j) =
+  let qs_i = qs !! i
+      qs_j = qs !! j
+  in (qs_i /= qs_j)
+      -- && (abs (qs_j - qs_i) /= (j - i))
+      && qs_j - qs_i /= j - i
+      && qs_j - qs_i /= i - j
+
+allQueensSafe :: Int -> [Queen] -> Bool
+allQueensSafe n qs =
+  (n == length qs)
+  && all (legal n) qs
+  && (all (queenPairSafe n qs) (indexPairs n))
+
+solveListCompN :: Int -> [Int]
+solveListCompN n =
+  head . filter (allQueensSafe n) $ [x | x <- mapM (const [1..n]) [1..n]]
+
+{-
+-- Gets all pairs of unique positions
+pairs :: Ord a => [a] -> [(a, a)]
+pairs xs = [(a, b) | a <- xs, b <- xs, a < b]
+
+-- Checks if all elements of list are unique
+allUnique :: Ord a => [a] -> Bool
+allUnique xs = length xs == length (nub xs)
+
+-- Check if two positions are safe
+pairSafe :: (Queen, Queen) -> Bool
+pairSafe ((x1, y1), (x2, y2)) =
+  -- No same x and y value
+  (x1 /= x2) && (y1 /= y2)
+  -- Not on the same diagonal
+  && (abs (x1 - x2) /= abs (y1 - y2))
+
+-- Check that all queens in a list are safe
+allSafe :: [Queen] -> Bool
+allSafe queens = all pairSafe $ pairs queens
+
+-- Valid Queens on an n x n board
+legalQueens :: Int -> [Queen] -> Bool
+legalQueens n queens =
+  (length queens == n)
+  && (n == length (nub queens))
+  && all (\(x, y) -> 1 <= x && x <= n && 1 <= y && y <= n) queens
+    -- && all (\p -> (1, 1) <= p && p <= (n, n)) queens
+
+-}
+
diff --git a/quasiquote/NQueens/Test.hs b/quasiquote/NQueens/Test.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/NQueens/Test.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module NQueens.Test where
+
+import NQueens.Encoding
+import G2.QuasiQuotes.QuasiQuotes
+
+{-
+queensTestN :: Int -> IO (Maybe [Queen])
+queensTestN n = [g2| \(n :: Int) -> ?(queens :: [Queen]) |
+                  legalQueens n queens
+                    && allSafe queens |] n
+-}
+
+queensTestN :: Int -> IO (Maybe [Queen])
+queensTestN num = [g2| \(n :: Int) -> ?(qs :: [Queen]) |
+                allQueensSafe n qs |] num
+
+
diff --git a/quasiquote/RegEx/RegEx.hs b/quasiquote/RegEx/RegEx.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/RegEx/RegEx.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module RegEx.RegEx where
+
+import Data.Data
+import G2.QuasiQuotes.G2Rep
+
+
+data RegEx = Empty | Epsilon | Atom Char
+  | Star RegEx | Concat RegEx RegEx | Or RegEx RegEx
+  deriving (Show, Eq, Data)
+
+$(derivingG2Rep ''RegEx)
+
+match :: RegEx -> String -> Bool
+match Empty _        = False
+match Epsilon s      = null s
+match (Atom x) s     = s == [x]
+match (Star _) []    = True
+match r@(Star x) s   = any (match2 x r)
+                           (splits [1..length s] s)
+match (Concat a b) s = any (match2 a b)
+                           (splits [0..length s] s)
+match (Or a b) s     = match a s || match b s
+
+match2 :: RegEx -> RegEx -> (String, String) -> Bool
+match2 a b (sa, sb)  = match a sa && match b sb
+
+splits :: [Int] -> [a] -> [([a], [a])]
+splits ns x = map (\n -> splitAt n x) ns
+
+
+
+
diff --git a/quasiquote/RegEx/Test.hs b/quasiquote/RegEx/Test.hs
new file mode 100644
--- /dev/null
+++ b/quasiquote/RegEx/Test.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module RegEx.Test where
+
+import RegEx.RegEx
+import G2.QuasiQuotes.QuasiQuotes
+
+regexTest1 :: IO (Maybe String)
+regexTest1 = stringSearch (Concat (Atom 'a') (Atom 'b'))
+
+regexTest2 :: IO (Maybe String)
+regexTest2 = stringSearch r
+  where
+    r = Concat
+          (Star (Or (Atom 'a') (Atom 'b')))
+          (Concat (Atom 'c')
+            (Or (Atom 'd')
+                (Concat (Atom 'e')
+                        (Atom 'f'))))
+                
+
+stringSearch :: RegEx -> IO (Maybe String)
+stringSearch = [g2| \(r :: RegEx) -> ?(str :: String) |
+              match r str |]
+
diff --git a/tests/CaseTest.hs b/tests/CaseTest.hs
new file mode 100644
--- /dev/null
+++ b/tests/CaseTest.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module CaseTest where
+
+import G2.Language
+import TestUtils
+
+exists1 :: [Expr] -> Bool
+exists1 [(App x y), (App z w)] =
+    dcHasName "A" x && dcHasName "B" y && dcHasName "A" z && dcHasName "C" w
+exists1 _ = False
+
+exists2 :: [Expr] -> Bool
+exists2 [x, y] = dcHasName "B" x && dcHasName "C" y
+exists2 _ = False
+
+exists3 :: [Expr] -> Bool
+exists3 [x, (App y (App z w))] =
+    dcHasName "C" x && dcHasName "A" y && dcHasName "A" z && dcHasName "B" w
+exists3 _ = False
+
+exists4 :: [Expr] -> Bool
+exists4 [_, (App y z)] = dcHasName "A" y && dcHasName "B" z
+exists4 _ = False
diff --git a/tests/DefuncTest.hs b/tests/DefuncTest.hs
new file mode 100644
--- /dev/null
+++ b/tests/DefuncTest.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module DefuncTest where
+
+import G2.Language
+import TestUtils
+
+-- Defunc1
+
+a :: Expr -> Expr
+a = App (Data $ DataCon (Name "A" (Just "Defunc1") 0 Nothing) (TyCon (Name "A" (Just "Defunc1") 0 Nothing) TYPE))
+
+dataB :: Expr
+dataB = Data $ DataCon (Name "B" (Just "Defunc1") 0 Nothing) (TyCon (Name "A" (Just "Defunc1") 0 Nothing) TYPE)
+
+add1 :: Expr
+add1 = Var (Id (Name "add1" (Just "Defunc1") 0 Nothing) tyIntS) 
+
+multiply2 :: Expr
+multiply2 = Var (Id (Name "multiply2" (Just "Defunc1") 0 Nothing) tyIntS) 
+
+defunc1Add1 :: [Expr] -> Bool
+defunc1Add1 [x, (App b (App _ y))] = x `eqIgT` a (add1) && b `eqIgT` dataB &&  y `eqIgT` (Lit $ LitInt 3)
+defunc1Add1 _ = False
+
+defunc1Multiply2 :: [Expr] -> Bool
+defunc1Multiply2 [x, (App b (App _ y))] = x `eqIgT` a (multiply2) && b `eqIgT` dataB && y `eqIgT` (Lit $ LitInt 4)
+defunc1Multiply2 _ = False
+
+defuncB :: [Expr] -> Bool
+defuncB [App x _, App y _] = x `eqIgT` dataB && y `eqIgT` dataB
+defuncB _ = False
+
+-- Defunc2
+
+add1D2 :: Expr
+add1D2 = Var (Id (Name "add1" (Just "Defunc2") 0 Nothing) tyIntS)
+
+sub1D2 :: Expr
+sub1D2 = Var (Id (Name "sub1" (Just "Defunc2") 0 Nothing) tyIntS)
+
+squareD2 :: Expr
+squareD2 = Var (Id (Name "square" (Just "Defunc2") 0 Nothing) tyIntS) 
+
+iListI :: Expr
+iListI = Data $ DataCon (Name "I" (Just "Defunc2") 0 Nothing) (TyCon (Name "IList" (Just "Defunc2") 0 Nothing) TYPE)
+
+iListNil :: Expr
+iListNil = Data $ DataCon (Name "INil" (Just "Defunc2") 0 Nothing) (TyCon (Name "IList" (Just "Defunc2") 0 Nothing) TYPE)
+
+fListF :: Expr
+fListF = Data $ DataCon (Name "F" (Just "Defunc2") 0 Nothing) (TyCon (Name "FList" (Just "Defunc2") 0 Nothing) TYPE)
+
+fListNil :: Expr
+fListNil = Data $ DataCon (Name "FNil" (Just "Defunc2") 0 Nothing) (TyCon (Name "FList" (Just "Defunc2") 0 Nothing) TYPE)
+
+add1Def :: Integer -> Integer
+add1Def x = x + 1
+
+sub1Def :: Integer -> Integer
+sub1Def x = x - 1
+
+squareDef :: Integer -> Integer
+squareDef x = x * x
+
+defunc2Check :: [Expr] -> Bool
+defunc2Check [flist, llist, llist'] = defunc2Check' flist llist llist'
+defunc2Check _ = False
+
+defunc2Check' :: Expr -> Expr -> Expr -> Bool
+defunc2Check' (App (App _ f) fs) 
+              (App (App _ (Lit (LitInt i))) is)
+              (App (App _ (Lit (LitInt i'))) is') = defunc2Check'' f i i' && defunc2Check' fs is is'
+defunc2Check' _ _ _ = True
+
+defunc2Check'' :: Expr -> Integer -> Integer -> Bool
+defunc2Check'' (Var (Id (Name "add1" _ _ _) _)) i i' = add1Def i == i'
+defunc2Check'' (Var (Id (Name "sub1" _ _ _) _)) i i' = sub1Def i == i'
+defunc2Check'' (Var (Id (Name "square" _ _ _) _)) i i' = squareDef i == i'
+defunc2Check'' _ _ _ = False
+
+tyIntS :: Type
+tyIntS = TyCon (Name "Int" Nothing 0 Nothing) TYPE
diff --git a/tests/Expr.hs b/tests/Expr.hs
new file mode 100644
--- /dev/null
+++ b/tests/Expr.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Expr (exprTests) where
+
+import G2.Language
+import qualified G2.Language.ExprEnv as E
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+exprTests :: IO TestTree
+exprTests = return exprTests'
+
+exprTests' :: TestTree
+exprTests' =
+    testGroup "Expr"
+    [ testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo1
+    , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo2
+    , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo3
+    , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo4
+    , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandToOverSat1 ]
+
+etaExpandTo1 :: Bool
+etaExpandTo1 =
+    let
+        (e, _) = etaExpandTo eenv (mkNameGen ()) 1 idF
+    in
+    case e of
+        (Lam TermL i (App _ (Var i'))) -> i == i'
+        _ -> False
+
+etaExpandTo2 :: Bool
+etaExpandTo2 =
+    let
+        (e, _) = etaExpandTo eenv (mkNameGen ()) 1 (Var (Id undefinedN (TyFun int int)))
+    in
+    case e of
+        Var (Id n (TyFun _ _)) -> n == undefinedN
+        _ -> False
+
+etaExpandTo3 :: Bool
+etaExpandTo3 =
+    let
+        (e, _) = etaExpandTo eenv (mkNameGen ()) 1
+                (Let [(fId, (Var (Id idN (TyFun int int))))] (Var fId))
+    in
+    case e of
+       (Lam TermL i (App (Let _ _) (Var i'))) -> i == i'
+       _ -> False
+
+etaExpandTo4 :: Bool
+etaExpandTo4 =
+    let
+        (e, _) = etaExpandTo eenv (mkNameGen ()) 1
+                (Let [(fId, (Var (Id undefinedN (TyFun int int))))] (Var fId))
+    in
+    case e of
+       Let [(i, _)] (Var i') -> i == fId && i' == fId
+       _ -> False
+
+etaExpandToOverSat1 :: Bool
+etaExpandToOverSat1 =
+    let
+        (e, _) = etaExpandTo eenv (mkNameGen ()) 3 idF
+    in
+    case e of
+        (Lam TermL i (App _ (Var i'))) -> i == i'
+        _ -> False
+
+-- DataCons
+intD :: DataCon
+intD = DataCon (Name "Int" Nothing 0 Nothing) int
+
+-- Types
+int :: Type
+int = TyCon (Name "Int" Nothing 0 Nothing) TYPE
+
+-- Typed Expr's
+x1N :: Name
+x1N = Name "x1" Nothing 0 Nothing
+
+fId :: Id
+fId = Id (Name "f" Nothing 0 Nothing) (TyFun int int)
+
+idN :: Name
+idN = Name "id" Nothing 0 Nothing
+
+idF :: Expr
+idF = Var $ Id idN (TyFun int int)
+
+bN :: Name
+bN = Name "b" Nothing 0 Nothing
+
+undefinedN :: Name
+undefinedN = Name "undefined" Nothing 0 Nothing
+
+eenv :: ExprEnv
+eenv = E.fromList [ (x1N, App (Data intD) (Lit (LitInt 1))) 
+                  , (idN, Lam TermL (Id bN int) (Var (Id bN int)))
+                  , (undefinedN, Prim Undefined TyBottom) ]
diff --git a/tests/GetNthTest.hs b/tests/GetNthTest.hs
new file mode 100644
--- /dev/null
+++ b/tests/GetNthTest.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module GetNthTest where
+
+import G2.Language
+import TestUtils
+
+data CList a = Cons a (CList a) | Nil
+
+data Peano = Succ Peano | Zero
+
+getNth :: CList Integer -> Integer -> Integer
+getNth (Cons x _)  0 = x 
+getNth (Cons _ xs) n = getNth xs (n - 1)
+getNth _      _ = -1
+
+getNthErr :: CList a -> Integer -> Maybe a 
+getNthErr (Cons x _)  0 = Just x 
+getNthErr (Cons _ xs) n = getNthErr xs (n - 1)
+getNthErr _      _ = Nothing
+
+toCList :: Expr -> CList Integer
+toCList (App (App (Data (DataCon (Name "Cons" _ _ _) _)) x) y) =
+    getInt x Nil $ \x' -> Cons x' (toCList y)
+toCList _ = Nil
+
+toCListGen :: Expr -> CList Expr
+toCListGen (App (App (Data (DataCon (Name "Cons" _ _ _) _)) e) y) =
+    Cons e (toCListGen y)
+toCListGen _ = Nil
+
+toCListType :: Expr -> CList Integer
+toCListType (App (App (App (Data (DataCon (Name "Cons" _ _ _) _)) (Type _)) x) y) =
+    getInt x Nil $ \x' -> Cons x' (toCListType y)
+toCListType _ = Nil
+
+toCListGenType :: Expr -> CList Expr
+toCListGenType (App (App (App (Data (DataCon (Name "Cons" _ _ _) _)) (Type _)) e) y) =
+    Cons e (toCListGenType y)
+toCListGenType _ = Nil
+
+cListLength :: CList a -> Integer
+cListLength (Cons _ xs) = 1 + cListLength xs
+cListLength Nil = 0
+
+getNthTest :: [Expr] -> Bool
+getNthTest [cl, i, a] = getIntB i $ \i' -> getIntB a $ \a' -> getNth (toCList cl) i' == a'
+getNthTest _ = False
+
+getNthErrTest :: [Expr] -> Bool
+getNthErrTest [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListType cl) i' == Nothing
+getNthErrTest [cl, i, a] = getIntB i $ \i' -> getIntB a $ \a' -> getNthErr (toCListType cl) i' == Just a'
+getNthErrTest _ = False
+
+getNthErrGenTest :: [Expr] -> Bool
+getNthErrGenTest [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing
+getNthErrGenTest [cl, i, e] =
+    case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of
+        Just e' -> e' `eqIgT` e
+        Nothing -> False
+getNthErrGenTest _ = False
+
+getNthErrGenTest' :: [Expr] -> Bool
+getNthErrGenTest' [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing
+getNthErrGenTest' [cl, i, e] =
+    case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of
+        Just e' -> e' `eqIgT` e
+        Nothing -> False
+getNthErrGenTest' _ = False
+
+getNthErrGenTest2 :: [Expr] -> Bool
+getNthErrGenTest2 [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing
+getNthErrGenTest2 [cl, i, e] =
+    case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of
+        Just e' -> e' `eqIgT` e
+        Nothing -> False
+getNthErrGenTest2 _ = False
+
+getNthErrGenTest2' :: [Expr] -> Bool
+getNthErrGenTest2' [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing
+getNthErrGenTest2' [cl, i, e] =
+    case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of
+        Just e' -> e' `eqIgT` e
+        Nothing -> False
+getNthErrGenTest2' _ = False
+
+elimType :: (ASTContainer m Expr) => m -> m
+elimType = modifyASTs elimType'
+
+elimType' :: Expr -> Expr
+elimType' (App e (Type _)) = e
+elimType' e = e
+
+getNthErrors :: [Expr] -> Bool
+getNthErrors [cl, App _ (Lit (LitInt i)), Prim Error _] = getNthErr (toCListGen cl) i == Nothing
+getNthErrors _ = False
+
+cfmapTest :: [Expr] -> Bool
+cfmapTest [_, e, e'] = cListLength (toCListGenType e) == cListLength (toCListGenType e') || isError e'
+cfmapTest _ = False
diff --git a/tests/HigherOrderMathTest.hs b/tests/HigherOrderMathTest.hs
new file mode 100644
--- /dev/null
+++ b/tests/HigherOrderMathTest.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module HigherOrderMathTest where
+
+import G2.Language
+
+import TestUtils
+
+abs2 :: Expr
+abs2 = Var (Id (Name "abs2" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+abs3 :: Expr
+abs3 = Var (Id (Name "abs3" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+square :: Expr
+square = Var (Id (Name "square" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+negativeSquare :: Expr
+negativeSquare = Var (Id (Name "negativeSquare" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+fourthPower :: Expr
+fourthPower = Var (Id (Name "fourthPower" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+add1 :: Expr
+add1 = Var (Id (Name "add1" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+sub1 :: Expr
+sub1 = Var (Id (Name "sub1" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+add :: Expr
+add = Var (Id (Name "add" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+sub :: Expr
+sub = Var (Id (Name "sub" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+approxSqrt :: Expr
+approxSqrt = Var (Id (Name "approxSqrt" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+pythagorean :: Expr
+pythagorean = Var (Id (Name "pythagorean" (Just "HigherOrderMath") 0 Nothing) tyBoolS)
+
+notNegativeAt0 :: Expr
+notNegativeAt0 = Var (Id (Name "notNegativeAt0" (Just "HigherOrderMath") 0 Nothing) TyBottom)
+
+notNegativeAt0NegativeAt1 :: Expr
+notNegativeAt0NegativeAt1 = Var (Id (Name "notNegativeAt0NegativeAt1" (Just "HigherOrderMath") 0 Nothing) TyBottom)
+
+abs2NonNeg :: [Expr] -> Bool
+abs2NonNeg [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` abs2 && x >= 0
+abs2NonNeg _ = False
+
+allabs2NonNeg :: [Expr] -> Bool
+allabs2NonNeg [f, App _ (Lit (LitFloat x)), _] = not (f `eqIgT` abs3) || x >= 0
+allabs2NonNeg _ = True
+
+squareRes :: [Expr] -> Bool
+squareRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` square && (x == 0 || x == 1)
+squareRes _ = False
+
+negativeSquareRes :: [Expr] -> Bool
+negativeSquareRes [f, _] = f `eqIgT` negativeSquare
+negativeSquareRes _ = False
+
+fourthPowerRes :: [Expr] -> Bool
+fourthPowerRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` square && (x == 0 || x == 1)
+fourthPowerRes _ = False
+
+addRes :: [Expr] -> Bool
+addRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` add && x > 0
+addRes _ = False
+
+subRes :: [Expr] -> Bool
+subRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` sub && x < 0
+subRes _ = False
+
+approxSqrtRes :: [Expr] -> Bool
+approxSqrtRes [f, App _ (Lit (LitFloat x))] = f `eqIgT` approxSqrt && x > 0
+approxSqrtRes _ = False
+
+pythagoreanRes :: [Expr] -> Bool
+pythagoreanRes [f, App _ (Lit (LitFloat x))] = f `eqIgT` pythagorean && x /= 0
+pythagoreanRes _ = False
+
+functionSatisfiesRes :: [Expr] -> Bool
+functionSatisfiesRes (Var (Id (Name "notNegativeAt0" _ _ _) _):Var (Id (Name"add1" _ _ _) _):_) = True
+functionSatisfiesRes _ = False
+
+tyBoolS :: Type
+tyBoolS = TyCon (Name "Bool" Nothing 0 Nothing) TYPE
diff --git a/tests/InputOutputTest.hs b/tests/InputOutputTest.hs
new file mode 100644
--- /dev/null
+++ b/tests/InputOutputTest.hs
@@ -0,0 +1,117 @@
+{-# LANGUAGE OverloadedStrings #-}
+module InputOutputTest ( checkInputOutput
+                       , checkInputOutputLH ) where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Control.Exception
+import qualified Data.Text as T
+import System.FilePath
+
+import G2.Config
+import G2.Initialization.MkCurrExpr
+import G2.Interface
+import G2.Language
+import G2.Liquid.Interface
+import G2.Translation
+
+import Reqs
+import TestUtils
+
+checkInputOutput :: FilePath -> String -> String -> Int -> Int -> [Reqs String] ->  IO TestTree
+checkInputOutput src md entry stps i req = checkInputOutputWithConfig [src] md entry i req (mkConfigTest {steps = stps})
+
+checkInputOutputWithConfig :: [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO TestTree
+checkInputOutputWithConfig src md entry i req config = do
+    r <- doTimeout (timeLimit config) $ checkInputOutput' src md entry i req config
+
+    let (b, e) = case r of
+            Nothing -> (False, "\nTimeout")
+            Just (Left e') -> (False, "\n" ++ show e')
+            Just (Right (b', _)) -> (b', "")
+
+    return . testCase (show src) $ assertBool ("Input/Output for file " ++ show src ++ " failed on function " ++ entry ++ "." ++ e) b 
+
+checkInputOutput' :: [FilePath] 
+                  -> String 
+                  -> String 
+                  -> Int 
+                  -> [Reqs String] 
+                  -> Config 
+                  -> IO (Either SomeException (Bool, [ExecRes ()]))
+checkInputOutput' src md entry i req config = try (checkInputOutput'' src md entry i req config)
+
+checkInputOutput'' :: [FilePath] 
+                   -> String 
+                   -> String 
+                   -> Int 
+                   -> [Reqs String] 
+                   -> Config 
+                   -> IO (Bool, [ExecRes ()])
+checkInputOutput'' src md entry i req config = do
+    let proj = map takeDirectory src
+    (mb_modname, exg2) <- translateLoaded proj src [] simplTranslationConfig config
+
+    let (init_state, _, bindings) = initState exg2 False (T.pack entry) mb_modname (mkCurrExpr Nothing Nothing) config
+    putStrLn "test"
+    
+    (r, _) <- runG2WithConfig init_state config bindings
+
+    let chAll = checkExprAll req
+    mr <- validateStates proj src md entry chAll [] r
+    let io = map (\(ExecRes { conc_args = i', conc_out = o}) -> i' ++ [o]) r
+
+    let chEx = checkExprInOutCount io i req
+    
+    return $ (mr && chEx, r)
+
+------------
+
+checkInputOutputLH :: [FilePath] -> [FilePath] -> String -> String -> Int -> Int -> [Reqs String] ->  IO TestTree
+checkInputOutputLH proj src md entry stps i req = checkInputOutputLHWithConfig proj src md entry i req (mkConfigTest {steps = stps})
+
+checkInputOutputLHWithConfig :: [FilePath] -> [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO TestTree
+checkInputOutputLHWithConfig proj src md entry i req config = do
+    r <- doTimeout (timeLimit config) $ checkInputOutputLH' proj src md entry i req config
+
+    let b = case r of
+            Just (Right b') -> b'
+            _ -> False
+
+    return . testCase (show src) $ assertBool ("Input/Output for file " ++ show src ++ " failed on function " ++ entry ++ ".") b
+
+checkInputOutputLH' :: [FilePath] -> [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO (Either SomeException Bool)
+checkInputOutputLH' proj src md entry i req config = try (checkInputOutputLH'' proj src md entry i req config)
+
+checkInputOutputLH'' :: [FilePath] -> [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO Bool
+checkInputOutputLH'' proj src md entry i req config = do
+    ((r, _), _) <- findCounterExamples proj src (T.pack entry) [] [] config
+
+    let chAll = checkExprAll req
+
+    mr <- validateStates proj src md entry chAll [] r
+    let io = map (\(ExecRes { conc_args = i', conc_out = o}) -> i' ++ [o]) r
+
+    let chEx = checkExprInOutCount io i req
+    return $ mr && chEx
+
+------------
+
+-- | Checks conditions on given expressions
+checkExprAll :: [Reqs String] -> [String]
+checkExprAll reqList = [f | RForAll f <- reqList]
+
+checkExprExists :: [Reqs String] -> [String]
+checkExprExists reqList = [f | RExists f <- reqList]
+
+checkExprInOutCount :: [[Expr]] -> Int -> [Reqs c] -> Bool
+checkExprInOutCount exprs i reqList =
+    let
+        checkAtLeast = and . map ((>=) (length exprs)) $ [x | AtLeast x <- reqList]
+        checkAtMost = and . map ((<=) (length exprs)) $ [x | AtMost x <- reqList]
+        checkExactly = and . map ((==) (length exprs)) $ [x | Exactly x <- reqList]
+
+        checkArgCount = and . map ((==) i . length) $ exprs
+    in
+    checkAtLeast && checkAtMost && checkExactly && checkArgCount
diff --git a/tests/PeanoTest.hs b/tests/PeanoTest.hs
new file mode 100644
--- /dev/null
+++ b/tests/PeanoTest.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module PeanoTest where
+
+import G2.Language
+
+import TestUtils
+
+zeroPeano :: Expr
+zeroPeano =
+    Data $ DataCon (Name "Zero" (Just "Peano") 0 Nothing) (TyCon (Name "Peano" (Just "Peano") 0 Nothing) TYPE)
+
+succPeano :: Expr -> Expr
+succPeano x =
+    App (Data $ DataCon (Name "Succ" (Just "Peano") 0 Nothing) (TyCon (Name "Peano" (Just "Peano") 0 Nothing) TYPE)) x
+
+peano_0_4 :: [Expr] -> Bool
+peano_0_4 [a, b, c] = a `eqIgT` zeroPeano && b `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+                      && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+peano_0_4 _ = False
+
+peano_1_3 :: [Expr] -> Bool
+peano_1_3 [a, b, c] = a `eqIgT` (succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano . succPeano $ zeroPeano)
+                   && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+peano_1_3 _ = False
+
+peano_1_4 :: [Expr] -> Bool
+peano_1_4 [a, b, c] = a `eqIgT` (succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+                      && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+peano_1_4 _ = False
+
+peano_2_2 :: [Expr] -> Bool
+peano_2_2 [a, b, c] = a `eqIgT` (succPeano . succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano $ zeroPeano)
+                   && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+peano_2_2 _ = False
+
+peano_3_1 :: [Expr] -> Bool
+peano_3_1 [a, b, c] = peano_1_3 [b, a, c]
+peano_3_1 _ = False
+
+peano_4_0 :: [Expr] -> Bool
+peano_4_0 [a, b, c] = peano_0_4 [b, a, c]
+peano_4_0 _ = False
+
+peano_4_1 :: [Expr] -> Bool
+peano_4_1 [a, b, c] = peano_1_4 [b, a, c]
+peano_4_1 _ = False
+
+peano_4_out :: [Expr] -> Bool
+peano_4_out [_, _, a] = a `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+peano_4_out _ = False
+
+peano_1_4_5 :: [Expr] -> Bool
+peano_1_4_5 [a, b, c] = a `eqIgT` (succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+                      && c `eqIgT` (succPeano . succPeano . succPeano . succPeano . succPeano $ zeroPeano)
+peano_1_4_5 _ = False
+
+peano_4_1_5 :: [Expr] -> Bool
+peano_4_1_5 [a, b, c] = peano_1_4_5 [b, a, c]
+peano_4_1_5 _ = False
diff --git a/tests/Reqs.hs b/tests/Reqs.hs
new file mode 100644
--- /dev/null
+++ b/tests/Reqs.hs
@@ -0,0 +1,68 @@
+module Reqs ( Reqs (..)
+            , checkExprGen
+            , checkAbsLHExprGen ) where
+
+import G2.Language
+
+-- | Requirements
+-- We use these to define checks on tests returning function inputs
+--     RForall f -- All the returned inputs satisfy the function f
+--     RExists f -- At least one of the returned inputs satisfies the function f
+--     AtLeast x -- At least x inputs are returned
+--     AtMost  x -- At most x inputs are returned
+--     Exactly x -- Exactly x inputs are returned
+data Reqs c = RForAll c
+              | RExists c
+              | AtLeast Int
+              | AtMost Int
+              | Exactly Int
+
+data TestErrors = BadArgCount
+                | TooMany
+                | TooFew
+                | NotExactly
+                | ArgsForAllFailed
+                | ArgsExistFailed deriving (Show)
+
+-- | Checks conditions on given expressions
+checkExprGen :: [[Expr]] -> Int -> [Reqs ([Expr] -> Bool)] -> Bool
+checkExprGen exprs i reqList =
+    let
+        argChecksAll = and . map (\f -> all (givenLengthCheck i f) exprs) $ [f | RForAll f <- reqList]
+        argChecksEx = and . map (\f -> any (givenLengthCheck i f) exprs) $ [f | RExists f <- reqList]
+        checkL = null $ checkLengths exprs i reqList
+    in
+    argChecksAll && argChecksEx && checkL
+
+givenLengthCheck :: Int -> ([Expr] -> Bool) -> [Expr] -> Bool
+givenLengthCheck i f e = if length e == i then f e else False
+
+checkAbsLHExprGen :: [(State [FuncCall], [Expr], Expr)] -> Int -> [Reqs ([Expr] -> Expr -> [FuncCall] -> Bool)] -> [TestErrors] 
+checkAbsLHExprGen exprs i reqList =
+    let
+        argChecksAll =
+            if and . map (\f -> all (\(s, es, e) -> lhGivenLengthCheck i f es e (track s)) exprs) $ [f | RForAll f <- reqList]
+                then []
+                else [ArgsForAllFailed]
+        argChecksEx =
+            if and . map (\f -> any (\(s, es, e) -> lhGivenLengthCheck i f es e (track s)) exprs) $ [f | RExists f <- reqList]
+                then []
+                else [ArgsExistFailed]
+        checkL = checkLengths (map (\(_, e, _) -> e) exprs) i reqList
+    in
+    argChecksAll ++ argChecksEx ++ checkL
+
+lhGivenLengthCheck :: Int -> ([Expr] -> Expr -> [FuncCall] -> Bool) -> [Expr] -> Expr -> [FuncCall] -> Bool
+lhGivenLengthCheck i f es e fc = if length es == i then f es e fc else False
+
+checkLengths :: [[Expr]] -> Int -> [Reqs c] -> [TestErrors]
+checkLengths exprs i reqList =
+    let
+        checkAtLeast = if and . map ((>=) (length exprs)) $ [x | AtLeast x <- reqList] then [] else [TooFew]
+        checkAtMost = if and . map ((<=) (length exprs)) $ [x | AtMost x <- reqList] then [] else [TooMany]
+        checkExactly = if and . map ((==) (length exprs)) $ [x | Exactly x <- reqList] then [] else [NotExactly]
+
+        checkArgCount = if and . map ((==) i . length) $ exprs then [] else [BadArgCount]
+    in
+    checkAtLeast ++ checkAtMost ++ checkExactly ++ checkArgCount
+
diff --git a/tests/TestUtils.hs b/tests/TestUtils.hs
new file mode 100644
--- /dev/null
+++ b/tests/TestUtils.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module TestUtils where
+
+import qualified Data.Map as M
+import Data.Monoid
+import qualified Data.Text as T
+
+import G2.Config
+import G2.Language
+
+mkConfigTest :: Config
+mkConfigTest = (mkConfig "/whatever/" [] M.empty)
+                    { higherOrderSolver = AllFuncs
+                    , timeLimit = 50
+                    , baseInclude = [ "./base-4.9.1.0/Control/Exception/"
+                                    , "./base-4.9.1.0/" ]
+                    , base = [ "./base-4.9.1.0/Control/Exception/Base.hs"
+                             , "./base-4.9.1.0/Prelude.hs" ]
+                    , extraDefaultMods = [] }
+
+mkConfigTestWithMap :: Config
+mkConfigTestWithMap =
+    mkConfigTest { baseInclude = baseInclude mkConfigTest ++ ["./base-4.9.1.0/Data/Internal/"]
+                 , base = base mkConfigTest ++ ["./base-4.9.1.0/Data/Internal/Map.hs"] }
+
+
+eqIgT :: Expr -> Expr -> Bool
+eqIgT (Var n) (Var n') = eqIgIds n n'
+eqIgT (Lit c) (Lit c') = c == c'
+eqIgT (Prim p _) (Prim p' _) = p == p'
+eqIgT (Lam _ n e) (Lam _ n' e') = eqIgIds n n' && e `eqIgT` e'
+eqIgT (App e1 e2) (App e1' e2') = e1 `eqIgT` e1' && e2 `eqIgT` e2'
+eqIgT (Data (DataCon n _)) (Data (DataCon n' _)) = eqIgNames n n'
+eqIgT (Type _) (Type _)= True
+eqIgT _ _ = False
+
+
+eqIgIds :: Id -> Id -> Bool
+eqIgIds (Id n _) (Id n' _) = eqIgNames n n'
+
+eqIgNames :: Name -> Name -> Bool
+eqIgNames (Name n m _ _) (Name n' m' _ _) = n == n' && m == m'
+
+typeNameIs :: Type -> T.Text -> Bool
+typeNameIs (TyCon n _) s = s == nameOcc n
+typeNameIs (TyApp t _) s = typeNameIs t s
+typeNameIs _ _ = False
+
+dcHasName :: T.Text -> Expr -> Bool
+dcHasName s (Data (DataCon n _)) = s == nameOcc n
+dcHasName _ _ = False
+
+isBool :: Expr -> Bool
+isBool (Data (DataCon _ (TyCon (Name "Bool" _ _ _) _))) = True
+isBool _ = False
+
+dcInAppHasName :: T.Text -> Expr -> Int -> Bool
+dcInAppHasName s (Data (DataCon n _)) 0 = s == nameOcc n
+dcInAppHasName s (App a _) n = dcInAppHasName s a (n - 1)
+dcInAppHasName _ _ _ = False
+
+buriedDCName :: T.Text -> Expr -> Bool
+buriedDCName s (App a _) = buriedDCName s a
+buriedDCName s (Data (DataCon n _)) = s == nameOcc n
+buriedDCName _ _ = False
+
+appNthArgIs :: Expr -> (Expr -> Bool) -> Int -> Bool
+appNthArgIs a f i = 
+    let
+        u = unApp a
+    in
+    case length u > i  of
+        True -> f (u !! i)
+        False -> False
+
+isInt :: Expr -> (Integer -> Bool) -> Bool
+isInt (Lit (LitInt x)) f = f x
+isInt (App _ (Lit (LitInt x))) f = f x
+isInt _ _ = False
+
+appNth :: Expr -> Int -> (Expr -> Bool) -> Bool
+appNth e 0 p = p e
+appNth (App _ e) i p = appNth e (i - 1) p
+appNth _ _ _ = False
+
+isIntT :: Type -> Bool
+isIntT (TyCon (Name "Int" _ _ _) _) = True
+isIntT _ = False
+
+isDouble :: Expr -> (Rational -> Bool) -> Bool
+isDouble (App _ (Lit (LitDouble x))) f = f x
+isDouble _ _ = False
+
+isFloat :: Expr -> (Rational -> Bool) -> Bool
+isFloat (Lit (LitFloat x)) f = f x
+isFloat (App _ (Lit (LitFloat x))) f = f x
+isFloat _ _ = False
+
+inCast :: Expr -> (Expr -> Bool) -> (Coercion -> Bool) -> Bool
+inCast (Cast e c) p q = p e && q c
+inCast _ _ _ = False
+
+notCast :: Expr -> Bool
+notCast (Cast _ _) = False
+notCast _ = True
+
+getInt :: Expr -> a -> (Integer -> a) -> a
+getInt (Lit (LitInt x)) _ f = f x
+getInt (App _ (Lit (LitInt x))) _ f = f x
+getInt _ x _ = x
+
+getIntB :: Expr -> (Integer -> Bool) -> Bool
+getIntB e = getInt e False
+
+getBoolB :: Expr -> (Bool -> Bool) -> Bool
+getBoolB (Data (DataCon n _)) f = f (nameOcc n == "True")
+getBoolB _ _ = False
+
+isApp :: Expr -> Bool
+isApp (App _ _) = True
+isApp _ = False
+
+isError :: Expr -> Bool
+isError (Prim Error _) = True
+isError _ = False
+
+isTyFun :: Type -> Bool
+isTyFun (TyFun _ _) = True
+isTyFun _ = False
+
+noUndefined :: Expr -> Bool
+noUndefined = getAll . evalASTs noUndefined'
+
+noUndefined' :: Expr -> All
+noUndefined' (Prim Undefined _) = All False
+noUndefined' _ = All True
diff --git a/tests/Typing.hs b/tests/Typing.hs
new file mode 100644
--- /dev/null
+++ b/tests/Typing.hs
@@ -0,0 +1,154 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Typing (typingTests) where
+
+import Prelude hiding (either, maybe)
+
+import G2.Language
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+typingTests :: IO TestTree
+typingTests = return typingTests'
+
+typingTests' :: TestTree
+typingTests' =
+    testGroup "Typing"
+    [
+      testCase "Function application" $ assertBool "Function application failed" test1
+    , testCase "Polymorphic DataCon application" $ assertBool "Polymorphic DataCon application failed" test2
+    , testCase "Polymorphic Function application" $ assertBool "Polymorphic Function application failed" test3
+    , testCase "Polymorphic Function application 2" $ assertBool "Polymorphic Function application 2 failed" test4
+    , testCase "Polymorphic Function application 3" $ assertBool "Polymorphic Function application 3 failed" funcAppTest
+    , testCase "Polymorphic Function" $ assertBool "Polymorphic Function failed" funcTest
+    , testCase "Kind application" $ assertBool "Kind application failed" tyAppKindTest
+
+    , testCase "Specializes test 1" $ assertBool ".:: failed" specTest1
+    , testCase "Specializes test 2" $ assertBool ".:: failed" specTest2
+    , testCase "Specializes test 3" $ assertBool ".:: failed" specTest3
+
+    , testCase "Specializes false test 1" $ assertBool ".:: failed" specFalseTest1
+    , testCase "Specializes false test 2" $ assertBool ".:: failed" specFalseTest2
+    ]
+
+test1 :: Bool
+test1 = typeOf (App f1 x1) == int
+
+test2 :: Bool
+test2 = typeOf (App (App just (Type int)) x1) == TyApp maybe int
+
+test3 :: Bool
+test3 = typeOf 
+        (App 
+            (App
+                f2 
+                (Type int)
+            )
+            x1
+        )
+        ==
+        int
+
+test4 :: Bool
+test4 = typeOf
+        (App 
+            (App
+                (App
+                    f3
+                    (Type int)
+                )
+                (Type float)
+            )
+            x1
+        )
+        ==
+        float
+
+funcAppTest :: Bool
+funcAppTest = typeOf (App (App idDef (Type int)) x1) == int
+
+funcTest :: Bool
+funcTest = idDef .:: (TyForAll (NamedTyBndr aid) (TyFun a a))
+
+tyAppKindTest :: Bool
+tyAppKindTest = typeOf (TyApp either a) == TyFun TYPE TYPE
+
+specTest1 :: Bool
+specTest1 = x1 .:: int
+
+specTest2 :: Bool
+specTest2 = x1 .:: a
+
+specTest3 :: Bool
+specTest3 = f2 .:: typeOf f3
+
+specFalseTest1 :: Bool
+specFalseTest1 = not $ Var (Id (Name "x1" Nothing 0 Nothing) a) .:: int
+
+specFalseTest2 :: Bool
+specFalseTest2 = not $ f3 .:: typeOf f2
+
+-- Typed Expr's
+x1 :: Expr
+x1 = Var $ Id (Name "x1" Nothing 0 Nothing) int
+
+f1 :: Expr
+f1 = Var $ Id (Name "f1" Nothing 0 Nothing) (TyFun int int)
+
+f2 :: Expr
+f2 = Var $ Id (Name "f2" Nothing 0 Nothing)
+                (TyForAll
+                    (NamedTyBndr bid)
+                    (TyFun b b)
+                )
+
+f3 :: Expr
+f3 = Var $ Id (Name "f3" Nothing 0 Nothing)
+                (TyForAll
+                    (NamedTyBndr bid)
+                    (TyForAll
+                        (NamedTyBndr aid)
+                        (TyFun b a)
+                    )
+                )
+
+just :: Expr
+just = Data $ DataCon 
+                    (Name "Just" Nothing 0 Nothing) 
+                    (TyForAll 
+                        (NamedTyBndr aid) 
+                        (TyFun a (TyApp maybe a))
+                    )
+
+idDef :: Expr
+idDef = Lam TypeL aid 
+            (Lam TermL
+                (Id (Name "x" Nothing 0 Nothing) a)
+                (Var (Id (Name "x" Nothing 0 Nothing) a))
+            )
+
+-- Types
+int :: Type
+int = TyCon (Name "Int" Nothing 0 Nothing) TYPE
+
+float :: Type
+float = TyCon (Name "Float" Nothing 0 Nothing) TYPE
+
+maybe :: Type
+maybe = TyCon (Name "Maybe" Nothing 0 Nothing) (TyFun TYPE TYPE)
+
+either :: Type
+either = TyCon (Name "Either" Nothing 0 Nothing) (TyFun TYPE (TyFun TYPE TYPE))
+
+a :: Type
+a = TyVar aid
+
+aid :: Id
+aid = Id (Name "a" Nothing 0 Nothing) TYPE
+
+b :: Type
+b = TyVar bid
+
+bid :: Id
+bid = Id (Name "b" Nothing 0 Nothing) TYPE