diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
index e10a5f0..9ff81a0 100644
--- a/copilot-verifier/copilot-verifier.cabal
+++ b/copilot-verifier/copilot-verifier.cabal
@@ -28,13 +28,13 @@ common bldflags
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot >= 3.17,
-    copilot-c99 >= 3.17,
-    copilot-core >= 3.17,
-    copilot-libraries >= 3.17,
-    copilot-language >= 3.17,
-    copilot-prettyprinter >= 3.17,
-    copilot-theorem >= 3.17,
+    copilot >= 3.18,
+    copilot-c99 >= 3.18,
+    copilot-core >= 3.18,
+    copilot-libraries >= 3.18,
+    copilot-language >= 3.18,
+    copilot-prettyprinter >= 3.18,
+    copilot-theorem >= 3.18,
     crucible,
     crucible-llvm,
     crux,
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs
index 3e93fab..70147e5 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs
@@ -15,7 +15,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "notIntMin" (forall (stream > constI32 minBound))
+  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))
   trigger "streamAbs" (abs stream == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs
index 85ae57b..5ae8696 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "notIntMax" (forall (stream < constI32 maxBound))
+  _ <- prop "notIntMax" (forAll (stream < constI32 maxBound))
   trigger "streamAddSigned" ((stream + 1) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs
index c812c65..5378693 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int16
       stream = extern "stream" Nothing
 
-  _ <- prop "nonzero" (forall (stream /= 0))
+  _ <- prop "nonzero" (forAll (stream /= 0))
   trigger "streamDiv" ((stream `div` stream) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs
index 1ba06f6..9e98acf 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs
@@ -18,7 +18,7 @@ spec = do
       stream2 :: Stream Word32
       stream2 = extern "stream2" Nothing
 
-  _ <- prop "withinBounds" (forall (stream2 < constW32 2))
+  _ <- prop "withinBounds" (forAll (stream2 < constW32 2))
   trigger "streamIndex" ((stream1 .!! stream2) == 1) [arg stream1, arg stream2]
 
 verifySpec :: Verbosity -> IO ()
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs
index ea658ca..c42f16c 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int16
       stream = extern "stream" Nothing
 
-  _ <- prop "nonzero" (forall (stream /= 0))
+  _ <- prop "nonzero" (forAll (stream /= 0))
   trigger "streamMod" ((stream `mod` stream) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs
index 1679bea..41f746b 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs
@@ -16,7 +16,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "withinRange" (forall
+  _ <- prop "withinRange" (forAll
            (constI32 ((minBound P.+ 1) P.* 2) < stream
          && stream < constI32 ((maxBound P.- 1) `P.div` 2)))
   trigger "streamMulSigned" ((stream * 2) == 2) [arg stream]
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs
index ac1c130..dbdcd8b 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs
@@ -18,7 +18,7 @@ spec = do
       stream2 :: Stream Int64
       stream2 = extern "stream2" Nothing
 
-  _ <- prop "lessThanBitWidth" (forall
+  _ <- prop "lessThanBitWidth" (forAll
          (constI64 0 <= stream2 && stream2 < constI64 32))
   trigger "streamShiftL" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]
 
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs
index c623015..12fe7c1 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs
@@ -18,7 +18,7 @@ spec = do
       stream2 :: Stream Int64
       stream2 = extern "stream2" Nothing
 
-  _ <- prop "lessThanBitWidth" (forall
+  _ <- prop "lessThanBitWidth" (forAll
          (constI64 0 <= stream2 && stream2 < constI64 32))
   trigger "streamShiftR" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]
 
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs
index df947ab..5503b17 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "notIntMin" (forall (stream > constI32 minBound))
+  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))
   trigger "streamSubSigned" ((stream - 1) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs
index ef8b383..58b75fb 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs
@@ -19,9 +19,9 @@ lastPrime = 31
 
 multRingSpec :: Spec
 multRingSpec = do
-  _ <- prop "clamp nonzero" (forall ((clamp > 0) && (clamp < lastPrime)))
-  _ <- prop "reduced" (forall (acc < lastPrime))
-  _ <- prop "nonzero" (forall (acc > 0 && (acc < lastPrime)))
+  _ <- prop "clamp nonzero" (forAll ((clamp > 0) && (clamp < lastPrime)))
+  _ <- prop "reduced" (forAll (acc < lastPrime))
+  _ <- prop "nonzero" (forAll (acc > 0 && (acc < lastPrime)))
 
   trigger "outofrange" (not (acc > 0 && acc < lastPrime)) [arg acc]
 
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs
index 1185c7a..7f9d8d3 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs
@@ -31,8 +31,8 @@ spec :: Spec
 spec = do
   observer "clk"  clkStream
   observer "clk'" clkStream'
-  _ <- prop "clksPhase" (forall (clkStream == drop 2 clkStream'))
-  _ <- prop "clksDistinct" (forall (not (clkStream && clkStream')))
+  _ <- prop "clksPhase" (forAll (clkStream == drop 2 clkStream'))
+  _ <- prop "clksDistinct" (forAll (not (clkStream && clkStream')))
   trigger "clksHigh" (clkStream && clkStream') []
 
 
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs
index 1b05ef0..708ea66 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs
@@ -38,9 +38,9 @@ bytecounter2 = counter true ([False] ++ bytecounter2 == 255)
 
 spec :: Spec
 spec =
-  do _ <- prop "range" (forall (bytecounter == unsafeCast (resetcounter `mod` 256)))
-     _ <- prop "range2" (forall (0 <= bytecounter2 && bytecounter2 <= 255))
-     _ <- prop "same"  (forall ((0 <= bytecounter2 && bytecounter2 <= 255) &&
+  do _ <- prop "range" (forAll (bytecounter == unsafeCast (resetcounter `mod` 256)))
+     _ <- prop "range2" (forAll (0 <= bytecounter2 && bytecounter2 <= 255))
+     _ <- prop "same"  (forAll ((0 <= bytecounter2 && bytecounter2 <= 255) &&
                                 (bytecounter == unsafeCast (resetcounter `mod` 256)) &&
                                 (bytecounter == bytecounter2)))
      trigger "counter" true [arg $ bytecounter, arg $ bytecounter2]
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs
index 843e717..f4c4a1d 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs
@@ -15,8 +15,8 @@ spec = do
       shiftBy :: Stream Int16
       shiftBy = extern "shiftBy" Nothing
 
-  _ <- prop "nonzero" (forall (stream /= 0))
-  _ <- prop "shiftByBits" (forall (0 <= shiftBy && shiftBy < 16))
+  _ <- prop "nonzero" (forAll (stream /= 0))
+  _ <- prop "shiftByBits" (forAll (0 <= shiftBy && shiftBy < 16))
 
   triggerOp1 "abs" abs stream
   triggerOp1 "signum" signum stream
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
index 17f8b4e..2cf989b 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
@@ -60,12 +60,12 @@ spec = do
 
   -- 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)
 
   -- Same as previous example, but in trigger form
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
index 9e28f06..1dd727e 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
@@ -170,8 +170,8 @@ horizontalWCV tvar s v =
   (((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)))
   trigger "well_clear_violation" (wcv tep s sz v vz) []
 
 verifySpec :: Verbosity -> IO ()
diff --git a/deps/copilot b/deps/copilot
index cfc565b..835deaf 160000
--- a/deps/copilot
+++ b/deps/copilot
@@ -1 +1 @@
-Subproject commit cfc565bcf52dd359eb7ee768549459402c1785df
+Subproject commit 835deafa4727c60741337a84cf7b8dce705f6e41