diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2019 Richard Cook
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,24 @@
+# sexpr-parser
+
+S-expression parser in Haskell
+
+## Description
+
+This is a [Megaparsec][megaparsec]-based parser for s-expression, heavily inspired by [lispparser][lispparser]. I'm building this to parse [SMT-LIB v2][smt-lib] output, so there.
+
+## Run Z3 demo
+
+The [Z3 demo](z3-demo/Main.hs) parses SMT-LIB v2 output from Z3. The executable assumes that you have [Z3][z3] installed and available on your system search path:
+
+```bash
+stack build --fast --exec sexpr-parser-z3-demo
+```
+
+## Licence
+
+[MIT License](LICENSE)
+
+[lispparser]: http://hackage.haskell.org/package/lispparser
+[megaparsec]: http://hackage.haskell.org/package/megaparsec
+[smt-lib]: http://smtlib.cs.uiowa.edu/language.shtml
+[z3]: https://github.com/Z3Prover/z3
diff --git a/lib/Text/SExpression.hs b/lib/Text/SExpression.hs
new file mode 100644
--- /dev/null
+++ b/lib/Text/SExpression.hs
@@ -0,0 +1,112 @@
+{-|
+Module      : Text.SExpression
+Description : S-expression parser
+Copyright   : (C) Richard Cook, 2019
+Licence     : MIT
+Maintainer  : rcook@rcook.org
+Stability   : stable
+Portability : portable
+
+This module provides a 'parseSExpr' function which parses simple
+s-expressions represented using the 'SExpr' type from 'String' input.
+
+Here's a full example which uses <https://github.com/Z3Prover/z3 Z3> to
+determine the satisfiability of a simple Boolean expression. It feeds
+<http://smtlib.cs.uiowa.edu/language.shtml SMT-LIB v2>-format input to
+Z3 and then parses the output (which uses a subset of Lisp-style
+s-expressions) to display the satisfying assignment for the expression.
+
+> module Main (main) where
+>
+> import Control.Applicative ((<|>))
+> import Control.Exception (evaluate)
+> import Control.Monad (void)
+> import Data.Foldable (for_)
+> import Data.List (sort)
+> import Data.Maybe (catMaybes)
+> import System.IO (BufferMode(..), hGetContents, hPutStrLn, hSetBuffering)
+> import System.Process
+> import Text.Megaparsec (parse)
+> import Text.Megaparsec.Char (char, string)
+> import Text.Printf (printf)
+> import Text.SExpression (Parser, SExpr(..), parseSExpr)
+>
+> data Z3SATResult = Satisfied | Unsatisfied deriving Show
+>
+> data Z3Output = Z3Output Z3SATResult SExpr deriving Show
+>
+> main :: IO ()
+> main = do
+>     result <- checkSATWithZ3 "input.smt2" $
+>         "(push)\n\
+>         \(declare-const x bool)\n\
+>         \(declare-const y bool)\n\
+>         \(assert (and (not x) y))\n\
+>         \(check-sat)\n\
+>         \(get-model)\n\
+>         \(pop)\n\
+>         \(exit)\n"
+>     case result of
+>         Left e -> putStrLn $ "Error: " ++ e
+>         Right (satResult, funs) -> do
+>             for_ funs $ \(name, value) ->
+>                 putStrLn $ printf "%s = %s" name (if value then "1" else "0")
+>             putStrLn $ "result=" ++ show satResult
+>
+> parseZ3SATResult :: Parser Z3SATResult
+> parseZ3SATResult = do
+>     s <- string "sat" <|> string "unsat"
+>     void $ char '\n'
+>     case s of
+>         "sat" -> pure Satisfied
+>         "unsat" -> pure Unsatisfied
+>         _ -> error "Unreachable"
+>
+> parseZ3Output :: Parser Z3Output
+> parseZ3Output = Z3Output <$> parseZ3SATResult <*> parseSExpr
+>
+> checkSATWithZ3 :: String -> String -> IO (Either String (Z3SATResult, [(String, Bool)]))
+> checkSATWithZ3 ctx input = do
+>     output <- withCreateProcess (proc "z3" ["-in"])
+>                         { std_in = CreatePipe
+>                         , std_out = CreatePipe
+>                         , std_err = Inherit
+>                         } $ \(Just hIn) (Just hOut) _ _ -> do
+>         hSetBuffering hIn NoBuffering
+>         hPutStrLn hIn input
+>         s <- hGetContents hOut
+>         void $ evaluate (length s)
+>         pure s
+>     case parse parseZ3Output ctx output of
+>         Left e -> pure $ Left (show e)
+>         Right (Z3Output satResult f) -> pure $ Right (satResult, sort (boolFuns f))
+>
+> boolFuns :: SExpr -> [(String, Bool)]
+> boolFuns (List (Atom "model" : fs)) = catMaybes $ map p fs
+>     where
+>         p :: SExpr -> Maybe (String, Bool)
+>         p (List [Atom "define-fun", Atom name, List [], Atom "bool", Atom "false"]) = Just (name, False)
+>         p (List [Atom "define-fun", Atom name, List [], Atom "bool", Atom "true"]) = Just (name, True)
+>         p _ = Nothing
+> boolFuns _ = []
+
+This demonstrates how to run the parser with 'Text.Megaparsec.parse' and
+'parseSExpr' as well as how to compose the s-expression parser with
+other parsers to handle a composite format. It also shows how to
+pattern-match on 'SExpr' to extract data from s-expressions.
+
+-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Text.SExpression
+    ( -- * Parser context
+      Parser
+    , -- * S-expression values
+      SExpr(..)
+    , -- * S-expression parser
+      parseSExpr
+    ) where
+
+import Text.SExpression.Internal (parseSExpr)
+import Text.SExpression.Types (Parser, SExpr(..))
diff --git a/lib/Text/SExpression/Internal.hs b/lib/Text/SExpression/Internal.hs
new file mode 100644
--- /dev/null
+++ b/lib/Text/SExpression/Internal.hs
@@ -0,0 +1,118 @@
+{-|
+Module      : Text.SExpression.Internal
+Description : Internal parser functions
+Copyright   : (C) Richard Cook, 2019
+Licence     : MIT
+Maintainer  : rcook@rcook.org
+Stability   : stable
+Portability : portable
+
+This module provides internal parser functions.
+-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Text.SExpression.Internal
+    ( -- * S-expression parser
+      parseSExpr
+    , -- * S-expression value parsers
+      parseAtom
+    , parseConsList
+    , parseList
+    , parseNumber
+    , parseQuoted
+    , parseString
+    ) where
+
+import Control.Applicative (empty)
+import Control.Monad (void)
+import Text.Megaparsec
+    ( (<|>)
+    , endBy
+    , many
+    , sepBy
+    , some
+    , try
+    )
+import Text.Megaparsec.Char
+    ( char
+    , digitChar
+    , letterChar
+    , noneOf
+    , oneOf
+    , space1
+    )
+import Text.Megaparsec.Char.Lexer
+    ( space
+    , skipLineComment
+    )
+import Text.SExpression.Types (Parser, SExpr(..))
+
+sc :: Parser ()
+sc = space space1 lineComment empty
+    where
+        lineComment = skipLineComment ";"
+
+symbol :: Parser Char
+symbol = oneOf "!$%&|*+-/:<=>?@^_~#"
+
+-- | S-expression parser
+parseSExpr ::
+    Parser SExpr    -- ^ parser
+parseSExpr =
+    parseAtom
+    <|> parseString
+    <|> parseNumber
+    <|> parseQuoted
+    <|> do
+            void $ char '('
+            lst <- (try parseList) <|> parseConsList
+            void $ char ')' >> sc
+            pure lst
+
+-- | Parse s-expression atom
+parseAtom ::
+    Parser SExpr    -- ^ parser
+parseAtom = do
+    h <- letterChar <|> symbol
+    t <- many (letterChar <|> digitChar <|> symbol)
+    let s = h : t
+    pure $ case s of
+                "#t" -> Bool True
+                "#f" -> Bool False
+                _ -> Atom s
+
+-- | Parse s-expression list
+parseList ::
+    Parser SExpr    -- ^ parser
+parseList = List <$> parseSExpr `sepBy` sc
+
+-- | Parse s-expression cons list
+parseConsList ::
+    Parser SExpr    -- ^ parser
+parseConsList = do
+    h <- parseSExpr `endBy` sc
+    t <- char '.' >> sc >> parseSExpr
+    pure $ ConsList h t
+
+-- | Parse s-expression number literal
+parseNumber ::
+    Parser SExpr    -- ^ parser
+parseNumber = (Number . read) <$> some digitChar
+
+-- | Parse s-expression string literal
+parseString ::
+    Parser SExpr    -- ^ parser
+parseString = do
+    void $ char '"'
+    s <- many (noneOf "\"")
+    void $ char '"'
+    pure $ String s
+
+-- | Parse s-expression quoted expression
+parseQuoted ::
+    Parser SExpr    -- ^ parser
+parseQuoted = do
+    void $ char '\''
+    e <- parseSExpr
+    pure $ List [Atom "quote", e]
diff --git a/lib/Text/SExpression/Types.hs b/lib/Text/SExpression/Types.hs
new file mode 100644
--- /dev/null
+++ b/lib/Text/SExpression/Types.hs
@@ -0,0 +1,34 @@
+{-|
+Module      : Text.SExpression.Types
+Description : Types
+Copyright   : (C) Richard Cook, 2019
+Licence     : MIT
+Maintainer  : rcook@rcook.org
+Stability   : stable
+Portability : portable
+
+This module provides parser context type 'Parser' and value type 'SExpr'.
+-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Text.SExpression.Types
+    ( Parser
+    , SExpr(..)
+    ) where
+
+import Data.Void (Void)
+import Text.Megaparsec (Parsec)
+
+-- | Parser context
+type Parser = Parsec Void String
+
+-- | S-expression values
+data SExpr =
+    Atom String                 -- ^ atom
+    | List [SExpr]              -- ^ list
+    | ConsList [SExpr] SExpr    -- ^ cons list
+    | Number Integer            -- ^ number literal
+    | String String             -- ^ string literal
+    | Bool Bool                 -- ^ Boolean literal
+    deriving (Eq, Read, Show)
diff --git a/sexpr-parser.cabal b/sexpr-parser.cabal
new file mode 100644
--- /dev/null
+++ b/sexpr-parser.cabal
@@ -0,0 +1,51 @@
+name:                   sexpr-parser
+version:                0.1.0.0
+synopsis:               Simple s-expression parser
+description:
+  This package provides a simple Megaparsec-based s-expression parser.
+homepage:               https://github.com/rcook/sexpr-parser#readme
+license:                MIT
+license-file:           LICENSE
+author:                 Richard Cook
+maintainer:             rcook@rcook.org
+copyright:              2019 Richard Cook
+category:               Command Line
+build-type:             Simple
+cabal-version:          >= 1.10
+extra-source-files:     README.md
+
+library
+  default-language:     Haskell2010
+  hs-source-dirs:       lib
+  exposed-modules:
+      Text.SExpression
+    , Text.SExpression.Internal
+    , Text.SExpression.Types
+  build-depends:
+      base >= 4.7 && < 5
+    , megaparsec
+    , parsec
+
+test-suite sexpr-parser-spec
+  type:                 exitcode-stdio-1.0
+  default-language:     Haskell2010
+  hs-source-dirs:       spec
+  main-is:              Spec.hs
+  other-modules:
+      Text.SExpression.InternalSpec
+  build-depends:
+      base >= 4.7 && < 5
+    , hspec
+    , megaparsec
+    , sexpr-parser
+
+executable sexpr-parser-z3-demo
+  default-language:     Haskell2010
+  hs-source-dirs:       z3-demo
+  main-is:              Main.hs
+  build-depends:
+      base >= 4.7 && < 5
+    , bytestring
+    , megaparsec
+    , process
+    , sexpr-parser
diff --git a/spec/Spec.hs b/spec/Spec.hs
new file mode 100644
--- /dev/null
+++ b/spec/Spec.hs
@@ -0,0 +1,11 @@
+{-|
+Module      : Text.SExpression.Spec
+Description : Tests
+Copyright   : (C) Richard Cook, 2019
+Licence     : MIT
+Maintainer  : rcook@rcook.org
+Stability   : stable
+Portability : portable
+-}
+
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
diff --git a/spec/Text/SExpression/InternalSpec.hs b/spec/Text/SExpression/InternalSpec.hs
new file mode 100644
--- /dev/null
+++ b/spec/Text/SExpression/InternalSpec.hs
@@ -0,0 +1,318 @@
+{-|
+Module      : Text.SExpression.InternalSpec
+Description : Tests
+Copyright   : (C) Richard Cook, 2019
+Licence     : MIT
+Maintainer  : rcook@rcook.org
+Stability   : stable
+Portability : portable
+-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Text.SExpression.InternalSpec (spec) where
+
+import Test.Hspec
+    ( Spec
+    , describe
+    , it
+    , shouldBe
+    )
+import Text.Megaparsec (parse)
+import Text.SExpression.Internal
+    ( parseAtom
+    , parseConsList
+    , parseList
+    , parseNumber
+    , parseQuoted
+    , parseSExpr
+    , parseString
+    )
+import Text.SExpression.Types (SExpr(..))
+
+spec :: Spec
+spec = do
+    describe "parseSExpr" $
+        it "parses test expressions" $ do
+            parse parseSExpr "" "assert" `shouldBe` Right (Atom "assert")
+            parse parseSExpr "" "(assert)" `shouldBe` Right (List [Atom "assert"])
+            parse parseSExpr "" "(assert (and))" `shouldBe` Right (List [Atom "assert", List [Atom "and"]])
+            parse parseSExpr "" "(assert (and (>)))" `shouldBe` Right (List [Atom "assert", List [Atom "and", List [Atom ">"]]])
+            parse parseSExpr "" "(assert (and (> (* 2 a) (+ b c)) (> (* 2 b) (+ c d))))" `shouldBe`
+                Right (List
+                        [ Atom "assert"
+                        , List
+                            [ Atom "and"
+                            , List
+                                [ Atom ">"
+                                , List
+                                    [ Atom "*"
+                                    , Number 2
+                                    , Atom "a"
+                                    ]
+                                , List
+                                    [ Atom "+"
+                                    , Atom "b"
+                                    , Atom "c"
+                                    ]
+                                ]
+                            , List
+                                [ Atom ">"
+                                , List
+                                    [ Atom "*"
+                                    , Number 2
+                                    , Atom "b"
+                                    ]
+                                , List
+                                    [ Atom "+"
+                                    , Atom "c"
+                                    , Atom "d"
+                                    ]
+                                ]
+                            ]
+                        ])
+    describe "parseAtom" $ do
+        it "parses #t" $
+            parse parseAtom "" "#t" `shouldBe` Right (Bool True)
+        it "parses #f" $
+            parse parseAtom "" "#f" `shouldBe` Right (Bool False)
+        it "parses single-character atom" $
+            parse parseAtom "" "x" `shouldBe` Right (Atom "x")
+        it "parses other atom" $
+            parse parseAtom "" "foo" `shouldBe` Right (Atom "foo")
+    describe "parseList" $
+        it "parses a list of different atoms" $
+            parse parseList "" "#t #f x foo 123" `shouldBe` Right (List [Bool True, Bool False, Atom "x", Atom "foo", Number 123])
+    describe "parseConsList" $
+        it "parses a cons list" $
+            parse parseConsList "" "123 . foo" `shouldBe` Right (ConsList [Number 123] (Atom "foo"))
+    describe "parseNumber" $
+        it "parses number literal" $
+            parse parseNumber "" "123" `shouldBe` Right (Number 123)
+    describe "parseString" $
+        it "parses string literal" $
+            parse parseString "" "\"foo\"" `shouldBe` Right (String "foo")
+    describe "parseQuoted" $
+        it "parses quoted expression" $
+            parse parseQuoted "" "'\"foo\"" `shouldBe` Right (List [Atom "quote", String "foo"])
+    describe "parseSExpr" $ do
+        it "parses Z3 output" $ do
+            let Right result = parse parseSExpr ""
+                                "(model\n\
+                                \(define-fun a4 () bool\n\
+                                \  false)\n\
+                                \(define-fun c3 () bool\n\
+                                \  true)\n\
+                                \(define-fun d4 () bool\n\
+                                \  false)\n\
+                                \(define-fun a2 () bool\n\
+                                \  true)\n\
+                                \(define-fun c5 () bool\n\
+                                \  false)\n\
+                                \(define-fun b4 () bool\n\
+                                \  true)\n\
+                                \(define-fun b5 () bool\n\
+                                \  true)\n\
+                                \(define-fun b2 () bool\n\
+                                \  false)\n\
+                                \(define-fun d1 () bool\n\
+                                \  true)\n\
+                                \(define-fun d2 () bool\n\
+                                \  false)\n\
+                                \(define-fun b1 () bool\n\
+                                \  false)\n\
+                                \(define-fun a5 () bool\n\
+                                \  true)\n\
+                                \(define-fun c2 () bool\n\
+                                \  true)\n\
+                                \(define-fun d3 () bool\n\
+                                \  true)\n\
+                                \(define-fun c4 () bool\n\
+                                \  true)\n\
+                                \(define-fun a1 () bool\n\
+                                \  false)\n\
+                                \(define-fun d5 () bool\n\
+                                \  false)\n\
+                                \(define-fun b3 () bool\n\
+                                \  true)\n\
+                                \(define-fun c0 () bool\n\
+                                \  false)\n\
+                                \(define-fun c1 () bool\n\
+                                \  true)\n\
+                                \(define-fun a3 () bool\n\
+                                \  true))"
+            result `shouldBe`
+                List
+                    [ Atom "model"
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "a4"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "c3"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "d4"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "a2"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "c5"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "b4"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "b5"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "b2"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "d1"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "d2"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "b1"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "a5"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "c2"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "d3"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "c4"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "a1"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "d5"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "b3"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "c0"
+                        , List []
+                        , Atom "bool"
+                        , Atom "false"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "c1"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    , List
+                        [ Atom "define-fun"
+                        , Atom "a3"
+                        , List []
+                        , Atom "bool"
+                        , Atom "true"
+                        ]
+                    ]
+        it "skips comments" $
+            parse parseSExpr "" "(aaa; a comment\nbbb ccc)"
+                `shouldBe` Right (List [Atom "aaa", Atom "bbb", Atom "ccc"])
+        it "handles trailing whitespace" $
+            parse parseSExpr "" "(model \n  (define-fun y () bool\n    true)\n  (define-fun x () bool\n    false)\n)\n"
+                `shouldBe` Right
+                    (List
+                        [ Atom "model"
+                        , List
+                            [ Atom "define-fun"
+                            , Atom "y"
+                            , List []
+                            , Atom "bool"
+                            , Atom "true"
+                            ]
+                        , List
+                            [ Atom "define-fun"
+                            , Atom "x"
+                            , List []
+                            , Atom"bool"
+                            , Atom "false"
+                            ]
+                        ]
+                    )
diff --git a/z3-demo/Main.hs b/z3-demo/Main.hs
new file mode 100644
--- /dev/null
+++ b/z3-demo/Main.hs
@@ -0,0 +1,85 @@
+{-|
+Module      : Main
+Description : Z3 demo
+Copyright   : (C) Richard Cook, 2019
+Licence     : MIT
+Maintainer  : rcook@rcook.org
+Stability   : stable
+Portability : portable
+-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Main (main) where
+
+import Control.Applicative ((<|>))
+import Control.Exception (evaluate)
+import Control.Monad (void)
+import Data.Foldable (for_)
+import Data.List (sort)
+import Data.Maybe (catMaybes)
+import System.IO (BufferMode(..), hGetContents, hPutStrLn, hSetBuffering)
+import System.Process
+import Text.Megaparsec (parse)
+import Text.Megaparsec.Char (char, string)
+import Text.Printf (printf)
+import Text.SExpression (Parser, SExpr(..), parseSExpr)
+
+data Z3SATResult = Satisfied | Unsatisfied deriving Show
+
+data Z3Output = Z3Output Z3SATResult SExpr deriving Show
+
+main :: IO ()
+main = do
+    result <- checkSATWithZ3 "input.smt2" $
+        "(push)\n\
+        \(declare-const x bool)\n\
+        \(declare-const y bool)\n\
+        \(assert (and (not x) y))\n\
+        \(check-sat)\n\
+        \(get-model)\n\
+        \(pop)\n\
+        \(exit)\n"
+    case result of
+        Left e -> putStrLn $ "Error: " ++ e
+        Right (satResult, funs) -> do
+            for_ funs $ \(name, value) ->
+                putStrLn $ printf "%s = %s" name (if value then "1" else "0")
+            putStrLn $ "result=" ++ show satResult
+
+parseZ3SATResult :: Parser Z3SATResult
+parseZ3SATResult = do
+    s <- string "sat" <|> string "unsat"
+    void $ char '\n'
+    case s of
+        "sat" -> pure Satisfied
+        "unsat" -> pure Unsatisfied
+        _ -> error "Unreachable"
+
+parseZ3Output :: Parser Z3Output
+parseZ3Output = Z3Output <$> parseZ3SATResult <*> parseSExpr
+
+checkSATWithZ3 :: String -> String -> IO (Either String (Z3SATResult, [(String, Bool)]))
+checkSATWithZ3 ctx input = do
+    output <- withCreateProcess (proc "z3" ["-in"])
+                        { std_in = CreatePipe
+                        , std_out = CreatePipe
+                        , std_err = Inherit
+                        } $ \(Just hIn) (Just hOut) _ _ -> do
+        hSetBuffering hIn NoBuffering
+        hPutStrLn hIn input
+        s <- hGetContents hOut
+        void $ evaluate (length s)
+        pure s
+    case parse parseZ3Output ctx output of
+        Left e -> pure $ Left (show e)
+        Right (Z3Output satResult f) -> pure $ Right (satResult, sort (boolFuns f))
+
+boolFuns :: SExpr -> [(String, Bool)]
+boolFuns (List (Atom "model" : fs)) = catMaybes $ map p fs
+    where
+        p :: SExpr -> Maybe (String, Bool)
+        p (List [Atom "define-fun", Atom name, List [], Atom "bool", Atom "false"]) = Just (name, False)
+        p (List [Atom "define-fun", Atom name, List [], Atom "bool", Atom "true"]) = Just (name, True)
+        p _ = Nothing
+boolFuns _ = []