diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,9 @@
+2023-09-07
+        * Version bump (3.16.1). (#455)
+        * Fix semantics of since in Copilot.Library.PTLTL. (#443)
+        * Prevent the majority function from generating unused local variables.
+          (#408)
+
 2023-07-07
         * Version bump (3.16). (#448)
 
diff --git a/copilot-libraries.cabal b/copilot-libraries.cabal
--- a/copilot-libraries.cabal
+++ b/copilot-libraries.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-libraries
-version:             3.16
+version:             3.16.1
 synopsis:            Libraries for the Copilot language.
 description:
   Libraries for the Copilot language.
@@ -41,7 +41,7 @@
                , containers       >= 0.4 && < 0.7
                , mtl              >= 2.0 && < 2.4
                , parsec           >= 2.0 && < 3.2
-               , copilot-language >= 3.16 && < 3.17
+               , copilot-language >= 3.16.1 && < 3.17
 
   exposed-modules:
       Copilot.Library.Libraries
diff --git a/src/Copilot/Library/PTLTL.hs b/src/Copilot/Library/PTLTL.hs
--- a/src/Copilot/Library/PTLTL.hs
+++ b/src/Copilot/Library/PTLTL.hs
@@ -39,8 +39,6 @@
   where
     tmp = [ False ] ++ s || tmp
 
--- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?
-since ::  Stream Bool -> Stream Bool -> Stream Bool
-since s1 s2 = alwaysBeen ( tmp ==> s1 )
-    where
-      tmp = eventuallyPrev $ [ False ] ++ s2
+-- | Is there a time when @s2@ holds and after which @s1@ continuously holds?
+since :: Stream Bool -> Stream Bool -> Stream Bool
+since s1 s2 = eventuallyPrev (s2 ==> (alwaysBeen s1))
diff --git a/src/Copilot/Library/Voting.hs b/src/Copilot/Library/Voting.hs
--- a/src/Copilot/Library/Voting.hs
+++ b/src/Copilot/Library/Voting.hs
@@ -56,7 +56,17 @@
   where
   inZero zero    = local (if zero then x else can) inCan
     where
-    inCan can'   = local (if zero || x == can then cnt+1 else cnt-1) inCnt
+    inCan can' =
+        -- We include a special case for when `xs` is empty that immediately
+        -- returns `can'`. We could omit this special case without changing the
+        -- final result, but this has the downside that `local` would bind a
+        -- local variable that would go unused in `inCnt`. (Note that `inCnt`
+        -- recursively invokes `majority'`, which doesn't use its last argument
+        -- if the list of vote streams is empty.) These unused local variables
+        -- would result in C code that triggers compiler warnings.
+        case xs of
+          [] -> can'
+          _  -> local (if zero || x == can then cnt+1 else cnt-1) inCnt
       where
       inCnt cnt' = majority' xs can' cnt'