diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,7 @@
+2025-09-07
+        * Version bump (4.5.1). (#666)
+        * Remove unused function Copilot.Theorem.Misc.SExpr.parseSExpr. (#661)
+
 2025-07-07
         * Version bump (4.5). (#642)
         * Removed unused pragmas. (#613)
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -14,7 +14,7 @@
   <https://copilot-language.github.io>.
 
 
-version                   : 4.5
+version                   : 4.5.1
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -54,7 +54,6 @@
                           , libBF                 >= 0.6.2 && < 0.7
                           , mtl                   >= 2.0 && < 2.4
                           , panic                 >= 0.4.0 && < 0.5
-                          , parsec                >= 2.0 && < 3.2
                           , parameterized-utils   >= 2.1.1 && < 2.2
                           , pretty                >= 1.0 && < 1.2
                           , process               >= 1.6 && < 1.7
@@ -63,8 +62,8 @@
                           , xml                   >= 1.3 && < 1.4
                           , what4                 >= 1.3 && < 1.8
 
-                          , copilot-core          >= 4.5 && < 4.6
-                          , copilot-prettyprinter >= 4.5 && < 4.6
+                          , copilot-core          >= 4.5.1 && < 4.6
+                          , copilot-prettyprinter >= 4.5.1 && < 4.6
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/src/Copilot/Theorem/Misc/SExpr.hs b/src/Copilot/Theorem/Misc/SExpr.hs
--- a/src/Copilot/Theorem/Misc/SExpr.hs
+++ b/src/Copilot/Theorem/Misc/SExpr.hs
@@ -2,10 +2,9 @@
 {-# LANGUAGE Safe              #-}
 
 -- | A representation for structured expression trees, with support for pretty
--- printing and for parsing.
+-- printing.
 module Copilot.Theorem.Misc.SExpr where
 
-import Text.ParserCombinators.Parsec
 import Text.PrettyPrint.HughesPJ as PP hiding (char, Str)
 
 import Control.Monad
@@ -70,37 +69,3 @@
         doc $$ indent (toDoc shouldIndent printAtom s)
       | otherwise =
         doc <+> toDoc shouldIndent printAtom s
-
--- | Parser for strings of characters separated by spaces into a structured
--- tree.
---
--- Parentheses are interpreted as grouping elements, that is, defining a
--- 'List', which may be empty.
-parser :: GenParser Char st (SExpr String)
-parser =
-  choice [try unitP, nodeP, leafP]
-
-  where
-    symbol     = oneOf "!#$%&|*+-/:<=>?@^_~."
-    lonelyStr  = many1 (alphaNum <|> symbol)
-
-    unitP      = string "()" >> return unit
-
-    leafP      = atom <$> lonelyStr
-
-    nodeP      = do void $ char '('
-                    spaces
-                    st <- sepBy parser spaces
-                    spaces
-                    void $ char ')'
-                    return $ List st
-
--- | Parser for strings of characters separated by spaces into a structured
--- tree.
---
--- Parentheses are interpreted as grouping elements, that is, defining a
--- 'List', which may be empty.
-parseSExpr :: String -> Maybe (SExpr String)
-parseSExpr str = case parse parser "" str of
-  Left s -> error (show s) -- Nothing
-  Right t -> Just t