diff --git a/horname.cabal b/horname.cabal
--- a/horname.cabal
+++ b/horname.cabal
@@ -1,5 +1,5 @@
 name:                horname
-version:             0.1.0.0
+version:             0.1.1.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
@@ -108,8 +108,12 @@
 
 simplify :: SExpr -> SExpr
 -- (* (- 1) x) → x
-simplify (List [StringLit "*", List [StringLit "-", IntLit 1], expr]) =
-  List [StringLit "-", expr]
+simplify (List [StringLit "*", List [StringLit "-", IntLit i], expr]) =
+  let expr' =
+        if i == 1
+          then expr
+          else List [StringLit "*", IntLit i, expr]
+  in List [StringLit "-", expr']
 -- merge nested ands
 simplify (List (StringLit "and":args)) =
   List (StringLit "and" : (andArgs ++ others))
@@ -139,7 +143,14 @@
     sepSubtraction (List [StringLit "-", arg1, arg2]) =
       [arg1, List [StringLit "-", 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 e = e
+
+negateExpr :: SExpr -> SExpr
+negateExpr (List [StringLit "not", expr]) = expr
+negateExpr expr = List [StringLit "not", expr]
 
 extractDefinitions :: Map Text [Text] -> [DefineFun] -> [DefineFun]
 extractDefinitions decls defs =
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
@@ -5,6 +5,7 @@
 import           Data.Generics.Uniplate.Data
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import           Data.Monoid
 import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Horname.Internal.SMT
@@ -15,7 +16,17 @@
 parseName = Text.pack <$> some (noneOf [' ', '\n', ')'])
 
 parseSort :: Parser Sort
-parseSort = Sort . Text.pack <$> some (noneOf [' ', '\n', ')'])
+parseSort = do
+  c <- noneOf [' ', '\n', ')']
+  case c of
+    '(' -> do
+      space
+      args <- map (\(Sort t) -> t) <$> sepBy parseSort someSpace
+      _ <- char ')'
+      pure $ Sort ("(" <> Text.intercalate " " args <> ")")
+    c' -> do
+      rest <- many (noneOf [' ', '\n', ')'])
+      pure (Sort (Text.pack (c' : rest)))
 
 parseArg :: Parser Arg
 parseArg = do