diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,7 @@
+2025-01-20
+        * Version bump (4.2). (#76)
+        * Reject specs that use multiple triggers with the same name. (#74)
+
 2024-11-08
         * Version bump (4.1). (#72)
 
diff --git a/copilot-verifier.cabal b/copilot-verifier.cabal
--- a/copilot-verifier.cabal
+++ b/copilot-verifier.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          copilot-verifier
-Version:       4.1
+Version:       4.2
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com
 Copyright:     (c) Galois, Inc 2021-2024
@@ -45,9 +45,9 @@
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot-c99 >= 4.1 && < 4.2,
-    copilot-core >= 4.1 && < 4.2,
-    copilot-theorem >= 4.1 && < 4.2,
+    copilot-c99 >= 4.2 && < 4.3,
+    copilot-core >= 4.2 && < 4.3,
+    copilot-theorem >= 4.2 && < 4.3,
     crucible >= 0.7.1 && < 0.8,
     crucible-llvm >= 0.7 && < 0.8,
     crux >= 0.7.1 && < 0.8,
@@ -78,9 +78,9 @@
   hs-source-dirs: examples
   build-depends:
     case-insensitive,
-    copilot >= 4.1 && < 4.2,
-    copilot-language >= 4.1 && < 4.2,
-    copilot-prettyprinter >= 4.1 && < 4.2,
+    copilot >= 4.2 && < 4.3,
+    copilot-language >= 4.2 && < 4.3,
+    copilot-prettyprinter >= 4.2 && < 4.3,
     copilot-verifier
   exposed-modules:
     Copilot.Verifier.Examples
diff --git a/src/Copilot/Verifier.hs b/src/Copilot/Verifier.hs
--- a/src/Copilot/Verifier.hs
+++ b/src/Copilot/Verifier.hs
@@ -23,7 +23,7 @@
   ) where
 
 import Control.Lens (view, (^.), to)
-import Control.Monad (foldM, forM_, when)
+import Control.Monad (foldM, forM_, unless, when)
 import Control.Monad.IO.Class (liftIO)
 import Control.Monad.State (execStateT, lift, StateT(..))
 import Data.Aeson (ToJSON)
@@ -33,7 +33,7 @@
 import qualified Data.Map.Strict as Map
 import Data.IORef (newIORef, modifyIORef', readIORef, IORef)
 import qualified Text.LLVM.AST as L
-import Data.List (genericLength)
+import Data.List (genericLength, sort)
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Vector as V
@@ -511,10 +511,26 @@
         let prepTrigger (nm, guard, _) =
               do gv <- freshGlobalVar halloc (Text.pack (nm ++ "_called")) NatRepr
                  return (nm, gv, guard)
-        triggerGlobals <- mapM prepTrigger (CW4.triggerState prfbundle)
 
+            checkDuplicateTriggerNames :: [Name] -> IO ()
+            checkDuplicateTriggerNames triggers =
+              traverse_ checkDuplicateTriggerName $ NE.group $ sort triggers
+
+            checkDuplicateTriggerName :: NonEmpty Name -> IO ()
+            checkDuplicateTriggerName (trig :| dupTrigs) =
+              unless (null dupTrigs) $
+                fail $ unlines
+                  [ "The specification invokes the `" ++ trig ++
+                    "` trigger function multiple times,"
+                  , "which copilot-verifier does not currently support."
+                  , "See https://github.com/Copilot-Language/copilot-verifier/issues/74."
+                  ]
+        let triggerState = CW4.triggerState prfbundle
+        checkDuplicateTriggerNames $ map (\(nm,_,_) -> nm) triggerState
+        triggerGlobals <- mapM prepTrigger triggerState
+
         -- execute the step function
-        let overrides = zipWith (triggerOverride clRefs) triggerGlobals (CW4.triggerState prfbundle)
+        let overrides = zipWith (triggerOverride clRefs) triggerGlobals triggerState
         mem'' <- executeStep opts csettings clRefs simctx memVar mem' llvmMod modTrans triggerGlobals overrides (CW4.assumptions prfbundle) (CW4.sideConds prfbundle)
 
         -- assert the poststate is in the relation