diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,11 @@
+2024-01-07
+        * Version bump (3.18). (#487)
+        * Enable tests for copilot-theorem in CI script. (#474)
+        * Enable tests for copilot-libraries in CI script. (#475)
+        * Replace uses of forall with forAll. (#470)
+        * Update CI job to check for MISRA compliance with cppcheck. (#472)
+        * Relax version constraint on optparse-applicative. (#488)
+
 2023-11-07
         * Version bump (3.17). (#466)
         * Replace uses of deprecated functions. (#457)
diff --git a/copilot.cabal b/copilot.cabal
--- a/copilot.cabal
+++ b/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             3.17
+version:             3.18
 cabal-version:       >= 1.10
 license:             BSD3
 license-file:        LICENSE
@@ -48,16 +48,16 @@
       -fno-warn-orphans
     build-depends:
                        base                  >= 4.9  && < 5
-                     , optparse-applicative  >= 0.14 && < 0.18
+                     , optparse-applicative  >= 0.14 && < 0.19
                      , directory             >= 1.3  && < 1.4
                      , filepath              >= 1.4  && < 1.5
 
-                     , copilot-core          >= 3.17 && < 3.18
-                     , copilot-theorem       >= 3.17 && < 3.18
-                     , copilot-language      >= 3.17 && < 3.18
-                     , copilot-libraries     >= 3.17 && < 3.18
-                     , copilot-c99           >= 3.17 && < 3.18
-                     , copilot-prettyprinter >= 3.17 && < 3.18
+                     , copilot-core          >= 3.18 && < 3.19
+                     , copilot-theorem       >= 3.18 && < 3.19
+                     , copilot-language      >= 3.18 && < 3.19
+                     , copilot-libraries     >= 3.18 && < 3.19
+                     , copilot-c99           >= 3.18 && < 3.19
+                     , copilot-prettyprinter >= 3.18 && < 3.19
 
 
     exposed-modules: Language.Copilot, Language.Copilot.Main
diff --git a/examples/WCV.hs b/examples/WCV.hs
--- a/examples/WCV.hs
+++ b/examples/WCV.hs
@@ -151,8 +151,8 @@
   (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr))
 
 spec = do
-  Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v)))
-  -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
+  Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))
+  -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
 
 main :: IO ()
 main = do
diff --git a/examples/what4/Arithmetic.hs b/examples/what4/Arithmetic.hs
--- a/examples/what4/Arithmetic.hs
+++ b/examples/what4/Arithmetic.hs
@@ -21,22 +21,22 @@
       efloat = extern "efloat" Nothing
 
   -- The simplest example involving numbers: equality on constant values.
-  void $ prop "Example 1" (forall ((constant (1 :: Int8)) == (constant 1)))
+  void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1)))
 
   -- Testing "a < a + 1". This should fail, because it isn't true.
-  void $ prop "Example 2" (forall (eint8 < (eint8 + 1)))
+  void $ prop "Example 2" (forAll (eint8 < (eint8 + 1)))
 
   -- Adding another condition to the above property to make it true.
-  void $ prop "Example 3" (forall ((eint8 < (eint8 + 1)) || (eint8 == 127)))
+  void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127)))
 
   -- Just like the previous example, but with words.
-  void $ prop "Example 4" (forall ((eword8 < (eword8 + 1)) || (eword8 == 255)))
+  void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255)))
 
   -- An example with floats.
-  void $ prop "Example 5" (forall ((2 * efloat) == (efloat + efloat)))
+  void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat)))
 
   -- Another example with floats. This fails, because it isn't true.
-  void $ prop "Example 6" (forall ((efloat + 1) /= efloat))
+  void $ prop "Example 6" (forAll ((efloat + 1) /= efloat))
 
 main :: IO ()
 main = do
diff --git a/examples/what4/Propositional.hs b/examples/what4/Propositional.hs
--- a/examples/what4/Propositional.hs
+++ b/examples/what4/Propositional.hs
@@ -13,38 +13,38 @@
 spec = do
   -- The constant value true, which is translated as the corresponding SMT
   -- boolean literal.
-  void $ prop "Example 1" (forall true)
+  void $ prop "Example 1" (forAll true)
 
   -- The constant value false, which is translated as the corresponding SMT
   -- boolean literal.
-  void $ prop "Example 2" (forall false)
+  void $ prop "Example 2" (forAll false)
 
   -- An inductively defined flavor of true, which requires induction to prove,
   -- and hence is found to be invalid by the SMT solver (since no inductive
   -- hypothesis is made).
   let a = [True] ++ a
-  void $ prop "Example 3" (forall a)
+  void $ prop "Example 3" (forAll a)
 
   -- An inductively defined "a or not a" proposition, which is unprovable by
   -- the SMT solver.
   let a = [False] ++ b
       b = [True] ++ a
-  void $ prop "Example 4" (forall (a || b))
+  void $ prop "Example 4" (forAll (a || b))
 
   -- A version of "a or not a" proposition which does not require any sort of
   -- inductive argument, and hence is provable.
   let a = [False] ++ b
       b = not a
-  void $ prop "Example 5" (forall (a || b))
+  void $ prop "Example 5" (forAll (a || b))
 
   -- A bit more convoluted version of Example 5, which is provable.
   let a = [True, False] ++ b
       b = [False] ++ not (drop 1 a)
-  void $ prop "Example 6" (forall (a || b))
+  void $ prop "Example 6" (forAll (a || b))
 
   -- An example using external streams.
   let a = extern "a" Nothing
-  void $ prop "Example 7" (forall (a || not a))
+  void $ prop "Example 7" (forAll (a || not a))
 
 main :: IO ()
 main = do
diff --git a/examples/what4/Structs.hs b/examples/what4/Structs.hs
--- a/examples/what4/Structs.hs
+++ b/examples/what4/Structs.hs
@@ -56,12 +56,12 @@
 
   -- Check equality, indexing into nested structs and arrays. Note that this is
   -- trivial by equality.
-  void $ prop "Example 1" $ forall $
+  void $ prop "Example 1" $ forAll $
     (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts)
 
   -- Same as previous example, but get a different array index (so should be
   -- false).
-  void $ prop "Example 2" $ forall $
+  void $ prop "Example 2" $ forAll $
     (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)
 
 main :: IO ()