diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
 # Revision history for ogma-core
 
+## [1.0.9] - 2023-05-21
+
+* Version bump 1.0.9 (#93).
+* Allow customizing the names of the C files generated by Copilot (#80).
+* Translate ZtoPre and YtoPre to Copilot (#86).
+
 ## [1.0.8] - 2023-03-21
 
 * Version bump 1.0.8 (#81).
diff --git a/ogma-core.cabal b/ogma-core.cabal
--- a/ogma-core.cabal
+++ b/ogma-core.cabal
@@ -32,7 +32,7 @@
 build-type:          Simple
 
 name:                ogma-core
-version:             1.0.8
+version:             1.0.9
 homepage:            http://nasa.gov
 license:             OtherLicense
 license-file:        LICENSE.pdf
@@ -109,13 +109,13 @@
     , IfElse
     , mtl
 
-    , ogma-extra              >= 1.0.8 && < 1.1
-    , ogma-language-c         >= 1.0.8 && < 1.1
-    , ogma-language-cocospec  >= 1.0.8 && < 1.1
-    , ogma-language-copilot   >= 1.0.8 && < 1.1
-    , ogma-language-fret-cs   >= 1.0.8 && < 1.1
-    , ogma-language-fret-reqs >= 1.0.8 && < 1.1
-    , ogma-language-smv       >= 1.0.8 && < 1.1
+    , ogma-extra              >= 1.0.9 && < 1.1
+    , ogma-language-c         >= 1.0.9 && < 1.1
+    , ogma-language-cocospec  >= 1.0.9 && < 1.1
+    , ogma-language-copilot   >= 1.0.9 && < 1.1
+    , ogma-language-fret-cs   >= 1.0.9 && < 1.1
+    , ogma-language-fret-reqs >= 1.0.9 && < 1.1
+    , ogma-language-smv       >= 1.0.9 && < 1.1
 
   hs-source-dirs:
     src
diff --git a/src/Command/FRETComponentSpec2Copilot.hs b/src/Command/FRETComponentSpec2Copilot.hs
--- a/src/Command/FRETComponentSpec2Copilot.hs
+++ b/src/Command/FRETComponentSpec2Copilot.hs
@@ -94,6 +94,7 @@
   { fretCS2CopilotUseCoCoSpec :: Bool
   , fretCS2CopilotIntType     :: String
   , fretCS2CopilotRealType    :: String
+  , fretCS2CopilotFilename    :: String
   }
 
 -- | Parse a JSON file containing a FRET component specification.
@@ -130,6 +131,7 @@
       (fretCS2CopilotUseCoCoSpec options)
       (fretCS2CopilotIntType options)
       (fretCS2CopilotRealType options)
+      (fretCS2CopilotFilename options)
 
 -- * Result
 
diff --git a/src/Command/FRETReqsDB2Copilot.hs b/src/Command/FRETReqsDB2Copilot.hs
--- a/src/Command/FRETReqsDB2Copilot.hs
+++ b/src/Command/FRETReqsDB2Copilot.hs
@@ -93,6 +93,7 @@
 -- to Copilot code.
 data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions
   { fretReqsDB2CopilotUseCoCoSpec :: Bool
+  , fretReqsDB2CopilotFilename    :: String
   }
 
 -- | Parse a JSON file containing a FRET requirement database.
@@ -127,6 +128,7 @@
 fretReqsDB2CopilotOptions options =
   T.FRETReqsDB2CopilotOptions
       (fretReqsDB2CopilotUseCoCoSpec options)
+      (fretReqsDB2CopilotFilename options)
 
 -- * Result
 
diff --git a/src/Language/Trans/CoCoSpec2Copilot.hs b/src/Language/Trans/CoCoSpec2Copilot.hs
--- a/src/Language/Trans/CoCoSpec2Copilot.hs
+++ b/src/Language/Trans/CoCoSpec2Copilot.hs
@@ -130,6 +130,8 @@
 -- operator.
 opOnePre2Copilot :: Op1Pre -> String
 opOnePre2Copilot Op1Pre    = "pre"
+opOnePre2Copilot Op1YtoPre = "pre"
+opOnePre2Copilot Op1ZtoPre = "tpre"
 opOnePre2Copilot Op1Once   = "PTLTL.eventuallyPrev"
 opOnePre2Copilot Op1Hist   = "PTLTL.alwaysBeen"
 opOnePre2Copilot Op1Y      = "PTLTL.previous"
diff --git a/src/Language/Trans/FRETComponentSpec2Copilot.hs b/src/Language/Trans/FRETComponentSpec2Copilot.hs
--- a/src/Language/Trans/FRETComponentSpec2Copilot.hs
+++ b/src/Language/Trans/FRETComponentSpec2Copilot.hs
@@ -57,6 +57,7 @@
   { fretCS2CopilotUseCoCoSpec :: Bool
   , fretCS2CopilotIntType     :: String
   , fretCS2CopilotRealType    :: String
+  , fretCS2CopilotFilename    :: String
   }
 
 -- | Transform a FRET TL specification into a Copilot specification.
@@ -86,6 +87,7 @@
       , pure clock
       , pure ftp
       , pure pre
+      , pure tpre
       , pure spec
       , pure main'
       ]
@@ -222,6 +224,12 @@
           , "pre = ([False] ++)"
           ]
 
+    -- Auxiliary streams: tpre
+    tpre = [ ""
+           , "tpre :: Stream Bool -> Stream Bool"
+           , "tpre = ([True] ++)"
+           ]
+
     -- Main specification
     spec :: [String]
     spec = [ ""
@@ -249,7 +257,8 @@
     main' :: [String]
     main' = [ ""
             , "main :: IO ()"
-            , "main = reify spec >>= compile \"fret\""
+            , "main = reify spec >>= compile \""
+                 ++ fretCS2CopilotFilename prefs ++ "\""
             ]
 
 -- | Return the corresponding type in Copilot matching a given FRET type.
diff --git a/src/Language/Trans/FRETReqsDB2Copilot.hs b/src/Language/Trans/FRETReqsDB2Copilot.hs
--- a/src/Language/Trans/FRETReqsDB2Copilot.hs
+++ b/src/Language/Trans/FRETReqsDB2Copilot.hs
@@ -62,6 +62,7 @@
 -- to Copilot code.
 data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions
   { fretReqsDB2CopilotUseCoCoSpec :: Bool
+  , fretReqsDB2CopilotFilename    :: String
   }
 
 -- | Return a string with the contents of the Copilot module that implements a
@@ -93,10 +94,12 @@
                               else SMV.boolSpecNames smvSpec
 
     sections | fretReqsDB2CopilotUseCoCoSpec prefs
-             = [ imports, propDef, externs, clock, ftp, undef, spec, main' ]
+             = [ imports, propDef, externs, clock, ftp, undef, tpre, spec
+               , main'
+               ]
 
              | otherwise
-             = [ imports, propDef, externs, clock, ftp, spec, main' ]
+             = [ imports, propDef, externs, clock, ftp, tpre, spec, main' ]
 
     imports :: [String]
     imports =
@@ -144,6 +147,11 @@
                , "pre = undefined"
                ]
 
+    tpre     = [ ""
+               , "tpre :: Stream Bool -> Stream Bool"
+               , "tpre = ([True] ++)"
+               ]
+
     spec     = [ ""
                , "-- | Complete specification. Calls the C function void handler(); when"
                , "-- the property is violated."
@@ -155,5 +163,6 @@
 
     main'    = [ ""
                , "main :: IO ()"
-               , "main = reify spec >>= compile \"fret\""
+               , "main = reify spec >>= compile \""
+                    ++ fretReqsDB2CopilotFilename prefs ++ "\""
                ]
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -110,6 +110,7 @@
                  { fretCS2CopilotUseCoCoSpec = False
                  , fretCS2CopilotIntType     = "Int64"
                  , fretCS2CopilotRealType    = "Float"
+                 , fretCS2CopilotFilename    = "fret"
                  }
     result <- fretComponentSpec2Copilot file opts
 
@@ -139,6 +140,7 @@
 testFretReqsDBCoCoSpec2Copilot file success = do
     let opts = FRETReqsDB2CopilotOptions
                  { fretReqsDB2CopilotUseCoCoSpec = True
+                 , fretReqsDB2CopilotFilename    = "fret"
                  }
     result <- fretReqsDB2Copilot file opts