diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Moritz Kiefer (c) 2016
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Moritz Kiefer nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,13 @@
+# horname
+
+[![Build Status](https://travis-ci.com/cocreature/horname.svg?token=k5tv9VjJ9pj7ynzqQyjR&branch=master)](https://travis-ci.com/cocreature/horname)
+
+Parses `define-fun` clauses output by SMT solvers
+and renames the variables according to annotations of the form
+
+```
+; :annot (INV_MAIN_42 i j n i j)
+```
+
+in the original SMT. The SMT-LIB standard itself does not allow naming
+arguments in a function declaration.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import qualified Data.Text.IO as Text
+import           Horname
+import           Options
+import           Options.Applicative hiding (Parser, runParser)
+
+main :: IO ()
+main = do
+  Opts outp inp <- execParser opts
+  outContent <- Text.readFile outp
+  inContent <- Text.readFile inp
+  case extractRenamedInvariants inp inContent outp outContent of
+    Left errs -> print errs
+    Right invariants -> mapM_ (Text.putStrLn . ppDefineFun) invariants
+  where
+    opts = info (helper <*> optsParser) (header "horname")
diff --git a/app/Options.hs b/app/Options.hs
new file mode 100644
--- /dev/null
+++ b/app/Options.hs
@@ -0,0 +1,18 @@
+module Options
+  ( Opts(..)
+  , optsParser
+  ) where
+
+import Data.Monoid
+import Options.Applicative
+
+data Opts = Opts
+  { solverOuptutFile :: !FilePath
+  , solverInputFile :: !FilePath
+  } deriving (Show, Eq, Ord)
+
+optsParser :: Parser Opts
+optsParser =
+  Opts <$>
+  strOption (long "smt-output" <> help "Path to the solver output") <*>
+  strOption (long "smt-input" <> help "Path to the input smt file")
diff --git a/horname.cabal b/horname.cabal
new file mode 100644
--- /dev/null
+++ b/horname.cabal
@@ -0,0 +1,42 @@
+name:                horname
+version:             0.1.0.0
+synopsis:            Rename function definitions returned by SMT solvers
+description:         Please see README.md
+homepage:            https://github.com/cocreature/horname#readme
+license:             BSD3
+license-file:        LICENSE
+author:              Moritz Kiefer
+maintainer:          value
+copyright:           (C) 2016 Moritz Kiefer
+category:            Web
+build-type:          Simple
+cabal-version:       >=1.10
+extra-source-files:  README.md
+tested-with:         GHC == 8.0.1
+
+executable horname
+  hs-source-dirs:      app
+  other-modules:       Options
+  main-is:             Main.hs
+  default-language:    Haskell2010
+  build-depends:       base >= 4.9 && < 5
+                     , horname
+                     , optparse-applicative >= 0.12 && < 0.14
+                     , text >= 1.2 && < 1.3
+  ghc-options:         -Wall
+
+library
+    hs-source-dirs:   src
+    exposed-modules:  Horname
+                      Horname.Internal.SMT
+                      Horname.Internal.SMT.Parser
+                      Horname.Internal.SMT.Pretty
+    default-language: Haskell2010
+    build-depends:    base >= 4.9 && < 5
+                    , containers >= 0.5 && < 0.6
+                    , megaparsec >= 5.0 && < 5.2
+                    , text >= 1.2 && < 1.3
+                    , these >= 0.7 && < 0.8
+                    , uniplate >= 1.6 && < 1.7
+                    , wl-pprint-text >= 1.1 && < 1.2
+    ghc-options:      -Wall
diff --git a/src/Horname.hs b/src/Horname.hs
new file mode 100644
--- /dev/null
+++ b/src/Horname.hs
@@ -0,0 +1,39 @@
+module Horname
+  ( extractRenamedInvariants
+  , DefineFun(..)
+  , ppDefineFun
+  , SExpr(..)
+  , VarName(..)
+  , Sort(..)
+  , Arg(..)
+  ) where
+
+import           Data.Text (Text)
+import qualified Data.Text.Lazy as Text
+import           Data.These
+import           Horname.Internal.SMT
+import           Horname.Internal.SMT.Parser
+import qualified Horname.Internal.SMT.Pretty as Pretty
+import           Text.Megaparsec
+import           Text.PrettyPrint.Leijen.Text
+
+extractRenamedInvariants
+  :: FilePath {- ^ input filename -}
+  -> Text {- ^ solver input -}
+  -> FilePath {- ^ output filename -}
+  -> Text {- ^ solver output -}
+  -> Either (These String String) [DefineFun]
+extractRenamedInvariants inpFile inp outpFile outp =
+  let outpResult = runParser parseDefineFuns outpFile outp
+      inpResult = runParser parseDeclareFuns inpFile inp
+  in case (outpResult, inpResult) of
+       (Left err, Left err') ->
+         Left (These (parseErrorPretty err) (parseErrorPretty err'))
+       (Left err, _) -> Left (This (parseErrorPretty err))
+       (_, Left err) -> Left (That (parseErrorPretty err))
+       (Right defineFuns, Right declareFuns) ->
+         Right (extractDefinitions declareFuns defineFuns)
+
+-- The magi numbers here are taken from hPutDoc
+ppDefineFun :: DefineFun -> Text
+ppDefineFun = Text.toStrict . displayT . renderPretty 0.4 80 . Pretty.ppDefineFun
diff --git a/src/Horname/Internal/SMT.hs b/src/Horname/Internal/SMT.hs
new file mode 100644
--- /dev/null
+++ b/src/Horname/Internal/SMT.hs
@@ -0,0 +1,149 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE LambdaCase #-}
+module Horname.Internal.SMT where
+
+import           Data.Data
+import           Data.List (foldl', find)
+import           Data.Map (Map)
+import qualified Data.Map as Map
+import           Data.Maybe
+import           Data.Text (Text)
+
+newtype VarName =
+  VarName Text
+  deriving (Show, Eq, Ord, Data)
+
+newtype Sort =
+  Sort Text
+  deriving (Show, Eq, Ord, Data)
+
+data Arg = Arg
+  { argName :: !VarName
+  , argSort :: !Sort
+  } deriving (Show, Eq, Ord, Data)
+
+data DefineFun = DefineFun
+  { funName :: !Text
+  , arguments :: ![Arg]
+  , returnSort :: !Sort
+  , body :: !SExpr
+  } deriving (Show, Eq, Ord, Data)
+
+data SExpr
+  = IntLit !Integer
+  | StringLit !Text
+  | List ![SExpr]
+  deriving (Show, Eq, Ord, Data)
+
+renameDefineFun :: [Text] -> DefineFun -> DefineFun
+renameDefineFun newNames (DefineFun n args retSort expr) =
+  DefineFun n renamedArgs retSort (renameInBody varMap expr)
+  where
+    renamedArgs =
+      zipWith (\(Arg _ sort) name -> Arg (VarName name) sort) args newNames
+    varMap :: Map Text Text
+    varMap =
+      Map.fromList $ zip (map (\(Arg (VarName name) _) -> name) args) newNames
+    renameInBody :: Map Text Text -> SExpr -> SExpr
+    renameInBody m (StringLit s) =
+      case Map.lookup s m of
+        Just s' -> StringLit s'
+        Nothing -> StringLit s
+    renameInBody _ (IntLit i) = IntLit i
+    renameInBody m (List exprs) = List (map (renameInBody m) exprs)
+
+insertBindings :: Map Text SExpr -> [SExpr] -> Map Text SExpr
+insertBindings m bindings = foldl' insertBinding m bindings
+
+insertBinding :: Map Text SExpr -> SExpr -> Map Text SExpr
+insertBinding m (List [StringLit key, val]) = Map.insert key val m
+insertBinding _ _ = error "Syntax error in let bindings"
+
+-- | This is not correct in the presence of nested lets but these
+-- should never occur in the Z3 output and Eldarica doesn’t include
+-- any lets.
+inlineLets :: SExpr -> SExpr
+inlineLets = inlineLets' Map.empty
+
+inlineLets' :: Map Text SExpr -> SExpr -> SExpr
+inlineLets' _ (IntLit i) = IntLit i
+inlineLets' m (StringLit t) =
+  case Map.lookup t m of
+    Just val -> val
+    Nothing -> StringLit t
+inlineLets' m (List [StringLit "let", List bindings, expr]) =
+  inlineLets' (insertBindings m bindings) expr
+inlineLets' m (List args) = List (map (inlineLets' m) args)
+
+comparisonOps :: [Text]
+comparisonOps = ["=", "<", "<=", ">", ">="]
+
+partitionPosNeg :: SExpr -> ([SExpr],[SExpr])
+partitionPosNeg (List (StringLit "+":args)) =
+  partition
+    (\case
+       (List [StringLit "-", e]) -> Right e
+       e -> Left e)
+    args
+partitionPosNeg e = ([e],[])
+
+partition               :: (a -> Either b c) -> [a] -> ([b],[c])
+partition p xs = foldr (select p) ([],[]) xs
+
+select :: (a -> Either b c) -> a -> ([b], [c]) -> ([b], [c])
+select p x (bs,cs) =
+  case p x of
+    Left b -> (b:bs,cs)
+    Right c -> (bs, c:cs)
+
+nonZero :: SExpr -> Bool
+nonZero (IntLit 0) = False
+nonZero _ = True
+
+sumExprs :: [SExpr] -> SExpr
+sumExprs [] = IntLit 0
+sumExprs [e] = e
+sumExprs args = List (StringLit "+" : args)
+
+simplify :: SExpr -> SExpr
+-- (* (- 1) x) → x
+simplify (List [StringLit "*", List [StringLit "-", IntLit 1], expr]) =
+  List [StringLit "-", expr]
+-- merge nested ands
+simplify (List (StringLit "and":args)) =
+  List (StringLit "and" : (andArgs ++ others))
+  where
+    (ands, others) =
+      partition
+        (\case
+           List (StringLit "and":args') -> Left args'
+           e -> Right e)
+        args
+    andArgs = concat ands
+-- Move negative and positive arguments to the same side of a comparison
+simplify (List [StringLit opName, arg1, arg2])
+  | opName `elem` comparisonOps =
+    case (partitionPosNeg arg1, partitionPosNeg arg2) of
+      ((posLeft, negLeft), (posRight, negRight)) ->
+        List
+          [ StringLit opName
+          , sumExprs . filter nonZero $ (posLeft ++ negRight)
+          , sumExprs . filter nonZero $ (posRight ++ negLeft)
+          ]
+-- Transform (+ a (- b c)) to (+ a b (- c))
+simplify (List (StringLit "+":args)) =
+  List (StringLit "+" : (sepSubtraction =<< args))
+  where
+    sepSubtraction :: SExpr -> [SExpr]
+    sepSubtraction (List [StringLit "-", arg1, arg2]) =
+      [arg1, List [StringLit "-", arg2]]
+    sepSubtraction e = [e]
+simplify e = e
+
+extractDefinitions :: Map Text [Text] -> [DefineFun] -> [DefineFun]
+extractDefinitions decls defs =
+  mapMaybe
+    (\(name, argNames) ->
+       renameDefineFun argNames <$> find ((== name) . funName) defs)
+    (Map.toList decls)
diff --git a/src/Horname/Internal/SMT/Parser.hs b/src/Horname/Internal/SMT/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Horname/Internal/SMT/Parser.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Horname.Internal.SMT.Parser where
+
+import           Data.Char
+import           Data.Generics.Uniplate.Data
+import           Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import           Data.Text (Text)
+import qualified Data.Text as Text
+import           Horname.Internal.SMT
+import           Text.Megaparsec
+import           Text.Megaparsec.Text
+
+parseName :: Parser Text
+parseName = Text.pack <$> some (noneOf [' ', '\n', ')'])
+
+parseSort :: Parser Sort
+parseSort = Sort . Text.pack <$> some (noneOf [' ', '\n', ')'])
+
+parseArg :: Parser Arg
+parseArg = do
+  _ <- char '('
+  name <- parseName
+  someSpace
+  sort <- parseSort
+  _ <- char ')'
+  pure (Arg (VarName name) sort)
+
+parseArgs :: Parser [Arg]
+parseArgs = do
+  _ <- char '('
+  args <- sepBy parseArg someSpace
+  _ <- char ')'
+  pure args
+
+someSpace :: Parser ()
+someSpace = skipSome spaceChar
+
+parseSExpr :: Parser SExpr
+parseSExpr = do
+  c <- char '(' <|> satisfy (not . isSpace)
+  case c of
+    '(' -> do
+      space
+      args <- sepBy parseSExpr someSpace
+      space
+      _ <- char ')'
+      pure (List args)
+    alphaNum
+      | isDigit alphaNum -> do
+        digits <- many digitChar
+        pure (IntLit (read (alphaNum : digits)))
+      | otherwise -> do
+        rest <- many (noneOf [' ', ')'])
+        pure . StringLit . Text.pack $ alphaNum : rest
+
+parseDefineFun :: Parser DefineFun
+parseDefineFun = do
+  _ <- manyTill anyChar (string "(define-fun")
+  someSpace
+  name <- parseName
+  someSpace
+  args <- parseArgs
+  someSpace
+  retSort <- parseSort
+  someSpace
+  expr <- parseSExpr
+  space
+  _ <- char ')'
+  pure (DefineFun name args retSort (transform simplify $ inlineLets expr))
+
+parseDefineFuns :: Parser [DefineFun]
+parseDefineFuns = many (try parseDefineFun)
+
+parseDeclareFun :: Parser (Text, [Text])
+parseDeclareFun = do
+  _ <- manyTill anyChar (string "; :annot (")
+  name <- parseName
+  someSpace
+  args <-
+    map (Text.replace "_0" "") <$>
+    sepBy parseName someSpace
+  space
+  _ <- char ')'
+  pure (name, args)
+
+parseDeclareFuns :: Parser (Map Text [Text])
+parseDeclareFuns = Map.fromList <$> many (try parseDeclareFun)
diff --git a/src/Horname/Internal/SMT/Pretty.hs b/src/Horname/Internal/SMT/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Horname/Internal/SMT/Pretty.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Horname.Internal.SMT.Pretty where
+
+import           Data.Text (Text)
+import qualified Data.Text.Lazy as Text
+import           Horname.Internal.SMT
+import           Text.PrettyPrint.Leijen.Text
+
+dontIndent :: [Text]
+dontIndent = ["+", "-", "*", "=", "<=", "<", ">=", ">"]
+
+ppSExpr :: SExpr -> Doc
+ppSExpr (IntLit i) = text . Text.pack $ show i
+ppSExpr (StringLit s) = text . Text.fromStrict $ s
+ppSExpr (List args'@(StringLit name:args))
+  | name `elem` dontIndent = parens $ hsep (map ppSExpr args')
+  | otherwise =
+    parens $ text (Text.fromStrict name) <+> align (vsep (map ppSExpr args))
+ppSExpr (List args) =
+  parens $ align (vsep (map ppSExpr args))
+
+ppSort :: Sort -> Doc
+ppSort (Sort t) = text (Text.fromStrict t)
+
+ppVarName :: VarName -> Doc
+ppVarName (VarName t) = text (Text.fromStrict t)
+
+ppArg :: Arg -> Doc
+ppArg (Arg name sort) = parens (ppVarName name <+> ppSort sort)
+
+ppDefineFun :: DefineFun -> Doc
+ppDefineFun (DefineFun name args retType expr) =
+  parens $
+  text "define-fun" <+>
+  align
+    (vsep
+       [ text (Text.fromStrict name)
+       , parens (hsep (map ppArg args)) <+> ppSort retType
+       , ppSExpr expr
+       ])