diff --git a/horname.cabal b/horname.cabal
--- a/horname.cabal
+++ b/horname.cabal
@@ -1,5 +1,5 @@
 name:                horname
-version:             0.1.2.0
+version:             0.1.3.0
 synopsis:            Rename function definitions returned by SMT solvers
 description:         Please see README.md
 homepage:            https://github.com/cocreature/horname#readme
diff --git a/src/Horname/Internal/SMT.hs b/src/Horname/Internal/SMT.hs
--- a/src/Horname/Internal/SMT.hs
+++ b/src/Horname/Internal/SMT.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
 module Horname.Internal.SMT where
 
 import           Data.Data
@@ -55,15 +56,15 @@
     renameInBody m (List exprs) = List (map (renameInBody m) exprs)
 
 insertBindings :: Map Text SExpr -> [SExpr] -> Map Text SExpr
-insertBindings m bindings = foldl' insertBinding m bindings
+insertBindings m bindings = foldl' (insertBinding m) 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"
+insertBinding :: Map Text SExpr -> Map Text SExpr -> SExpr -> Map Text SExpr
+insertBinding oldMap m (List [StringLit key, val]) = Map.insert key (inlineLets' oldMap 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.
+-- | This is not correct in the case of quantifiers but ignoring this
+-- simplifies the implementation and seems to be enough for z3 and
+-- eldarica
 inlineLets :: SExpr -> SExpr
 inlineLets = inlineLets' Map.empty
 
@@ -87,7 +88,8 @@
        (List [StringLit "-", e]) -> Right e
        e -> Left e)
     args
-partitionPosNeg e = ([e],[])
+partitionPosNeg (Neg e) = ([], [e])
+partitionPosNeg e = ([e], [])
 
 partition               :: (a -> Either b c) -> [a] -> ([b],[c])
 partition p xs = foldr (select p) ([],[]) xs
@@ -107,28 +109,60 @@
 sumExprs [e] = e
 sumExprs args = List (StringLit "+" : args)
 
+pattern And :: [SExpr] -> SExpr
+pattern And args = List (StringLit "and" : args)
+
+pattern Neg :: SExpr -> SExpr
+pattern Neg arg = List [StringLit "-", arg]
+
+pattern Or :: [SExpr] -> SExpr
+pattern Or args = List (StringLit "or" : args)
+
+pattern BinOp :: Text -> SExpr -> SExpr -> SExpr
+pattern BinOp name op1 op2 = List [StringLit name, op1, op2]
+
 -- first pass of simplifications
 simplify :: SExpr -> SExpr
 -- (* (- 1) x) → x
-simplify (List [StringLit "*", List [StringLit "-", IntLit i], expr]) =
+simplify (BinOp "*" (Neg (IntLit i)) expr) =
   let expr' =
         if i == 1
           then expr
-          else List [StringLit "*", IntLit i, expr]
-  in List [StringLit "-", expr']
+          else BinOp "*" (IntLit i) expr
+  in Neg expr'
 -- merge nested ands
-simplify (List (StringLit "and":args)) =
-  List (StringLit "and" : (andArgs ++ others))
+simplify (And args) = And (andArgs ++ others)
   where
     (ands, others) =
       partition
         (\case
-           List (StringLit "and":args') -> Left args'
+           And args' -> Left args'
            e -> Right e)
         args
     andArgs = concat ands
+-- pull out common subexpressions of disjunctions
+simplify (Or (arg:args)) =
+  if null commonSubExprs
+    then Or (arg : args)
+    else And
+           (commonSubExprs ++
+            [Or (map (removeSubExprs commonSubExprs) (arg : args))])
+  where
+    commonSubExprs =
+      filter
+        (\arg' -> all (arg' `subsumedBy`) args)
+        (case arg of
+           And exprs -> exprs
+           _ -> [])
+    subsumedBy :: SExpr -> SExpr -> Bool
+    subsumedBy e (And args') = e `elem` args'
+    subsumedBy _ _ = False
+    removeSubExprs :: [SExpr] -> SExpr -> SExpr
+    removeSubExprs subExprs (And exprs) =
+      And (filter (\e -> not (e `elem` subExprs)) exprs)
+    removeSubExprs _ e = e
 -- Move negative and positive arguments to the same side of a comparison
-simplify (List [StringLit opName, arg1, arg2])
+simplify (BinOp opName arg1 arg2)
   | opName `elem` comparisonOps =
     case (partitionPosNeg arg1, partitionPosNeg arg2) of
       ((posLeft, negLeft), (posRight, negRight)) ->
@@ -142,12 +176,10 @@
   List (StringLit "+" : (sepSubtraction =<< args))
   where
     sepSubtraction :: SExpr -> [SExpr]
-    sepSubtraction (List [StringLit "-", arg1, arg2]) =
-      [arg1, List [StringLit "-", arg2]]
+    sepSubtraction (BinOp "-" arg1 arg2) = [arg1, Neg arg2]
     sepSubtraction e = [e]
 -- transform (not (or (not …))) to (and …)
-simplify (List [StringLit "not", List (StringLit "or":args)]) =
-  List (StringLit "and" : map negateExpr args)
+simplify (List [StringLit "not", Or args]) = And (map negateExpr args)
 simplify e = e
 
 antiSymmetricOp :: Text -> Bool
@@ -155,8 +187,7 @@
 -- second pass of simplifications
 simplify' :: SExpr -> SExpr
 -- transform two inequalities to an equality
-simplify' (List (StringLit "and":args)) =
-  List (StringLit "and" : other ++ mergeInequalities inequality)
+simplify' (And args) = And (other ++ mergeInequalities inequality)
   where
     (inequality, other) =
       List.partition
@@ -169,7 +200,7 @@
     mergeInequalities (e@(List [StringLit op, expr1, expr2]):rest) =
       let reversedE = List [StringLit op, expr2, expr1]
       in if reversedE `elem` rest
-           then List [StringLit "=", expr1, expr2] :
+           then BinOp "=" expr1 expr2 :
                 mergeInequalities (filter (not . (`elem` [e, reversedE])) rest)
            else e : mergeInequalities rest
     mergeInequalities (e:es) = e : mergeInequalities es
diff --git a/src/Horname/Internal/SMT/Parser.hs b/src/Horname/Internal/SMT/Parser.hs
--- a/src/Horname/Internal/SMT/Parser.hs
+++ b/src/Horname/Internal/SMT/Parser.hs
@@ -62,7 +62,7 @@
         digits <- many digitChar
         pure (IntLit (read (alphaNum : digits)))
       | otherwise -> do
-        rest <- many (noneOf [' ', ')'])
+        rest <- many (noneOf [' ', '\t', '\n', ')'])
         pure . StringLit . Text.pack $ alphaNum : rest
 
 parseDefineFun :: Parser DefineFun