diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2025-07-07
+        * Version bump (4.5). (#642)
+        * Removed unused pragmas. (#613)
+        * Relax version constraint on what4. (#611)
+
 2025-05-07
         * Version bump (4.4). (#618)
         * Translate quantifiers correctly in Kind2 backend. (#594)
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.4
+version                   : 4.5
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -61,10 +61,10 @@
                           , random                >= 1.1 && < 1.3
                           , transformers          >= 0.5 && < 0.7
                           , xml                   >= 1.3 && < 1.4
-                          , what4                 >= 1.3 && < 1.7
+                          , what4                 >= 1.3 && < 1.8
 
-                          , copilot-core          >= 4.4 && < 4.5
-                          , copilot-prettyprinter >= 4.4 && < 4.5
+                          , copilot-core          >= 4.5 && < 4.6
+                          , copilot-prettyprinter >= 4.5 && < 4.6
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/src/Copilot/Theorem/Kind2/Prover.hs b/src/Copilot/Theorem/Kind2/Prover.hs
--- a/src/Copilot/Theorem/Kind2/Prover.hs
+++ b/src/Copilot/Theorem/Kind2/Prover.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE LambdaCase  #-}
 {-# LANGUAGE Trustworthy #-}
 
 -- | A prover backend based on Kind2.
diff --git a/src/Copilot/Theorem/Prover/SMTIO.hs b/src/Copilot/Theorem/Prover/SMTIO.hs
--- a/src/Copilot/Theorem/Prover/SMTIO.hs
+++ b/src/Copilot/Theorem/Prover/SMTIO.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE LambdaCase     #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RankNTypes     #-}
 {-# LANGUAGE Safe           #-}
diff --git a/src/Copilot/Theorem/What4.hs b/src/Copilot/Theorem/What4.hs
--- a/src/Copilot/Theorem/What4.hs
+++ b/src/Copilot/Theorem/What4.hs
@@ -1,18 +1,13 @@
-{-# LANGUAGE DataKinds                  #-}
-{-# LANGUAGE FlexibleContexts           #-}
-{-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE KindSignatures             #-}
-{-# LANGUAGE LambdaCase                 #-}
-{-# LANGUAGE MultiWayIf                 #-}
-{-# LANGUAGE PatternSynonyms            #-}
-{-# LANGUAGE RankNTypes                 #-}
-{-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE StandaloneDeriving         #-}
-{-# LANGUAGE TemplateHaskell            #-}
-{-# LANGUAGE TupleSections              #-}
-{-# LANGUAGE TypeApplications           #-}
-{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE PatternSynonyms     #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeOperators       #-}
 
 -- |
 -- Module      : Copilot.Theorem.What4