diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs
index 949726030b7a..f71bc535a11e 100644
--- a/tools/compiletest/src/common.rs
+++ b/tools/compiletest/src/common.rs
@@ -10,6 +10,7 @@ use std::path::{Path, PathBuf};
 use std::str::FromStr;
 
 use std::time::Duration;
+use test::test::TestTimeOptions;
 use test::ColorConfig;
 
 #[derive(Clone, Copy, Eq, PartialEq, Debug)]
@@ -145,6 +146,14 @@ pub struct Config {
     /// updating multiple tests. Users should still manually edit the files after to only keep
     /// relevant expectations.
     pub fix_expected: bool,
+
+    /// Whether we should measure and limit the time of a test.
+    pub time_opts: Option<TestTimeOptions>,
+
+    /// Extra arguments to be passed to Kani in this regression.
+    /// Note that there is no validation done whether these flags conflict with existing flags.
+    /// For example, one could add `--kani-flag=--only-codegen` to only compile all tests.
+    pub extra_args: Vec<String>,
 }
 
 #[derive(Debug, Clone)]
diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs
index 89e3603a8510..afbee19e6ade 100644
--- a/tools/compiletest/src/header.rs
+++ b/tools/compiletest/src/header.rs
@@ -37,7 +37,7 @@ impl TestProps {
     pub fn from_file(testfile: &Path, config: &Config) -> Self {
         let mut props = TestProps::new();
         props.load_from(testfile, config);
-
+        props.kani_flags.extend(config.extra_args.iter().cloned());
         props
     }
 
diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs
index 98a12f3d1ea3..0dd403ba1b2f 100644
--- a/tools/compiletest/src/main.rs
+++ b/tools/compiletest/src/main.rs
@@ -21,6 +21,7 @@ use std::io::{self};
 use std::path::{Path, PathBuf};
 use std::str::FromStr;
 use std::time::{Duration, SystemTime};
+use test::test::TestTimeOptions;
 use test::ColorConfig;
 use tracing::*;
 use walkdir::WalkDir;
@@ -90,6 +91,14 @@ pub fn parse_config(args: Vec<String>) -> Config {
         .optflag("", "dry-run", "don't actually run the tests")
         .optflag("", "fix-expected",
         "override all expected files that did not match the output. Tests will NOT fail when there is a mismatch")
+        .optflag("", "report-time",
+                 "report the time of each test. Configuration is done via env variables, like \
+                 rust unit tests.")
+        .optmulti("", "kani-flag", 
+                  "pass extra flags to Kani. Note that this may cause spurious failures if the \
+                  passed flag conflicts with the test configuration. Only works for `kani`, \
+                  `cargo-kani`, and `expected` modes."
+                  , "ARG")
     ;
 
     let (argv0, args_) = args.split_first().unwrap();
@@ -164,6 +173,10 @@ pub fn parse_config(args: Vec<String>) -> Config {
         dry_run: matches.opt_present("dry-run"),
         fix_expected: matches.opt_present("fix-expected"),
         timeout,
+        time_opts: matches
+            .opt_present("report-time")
+            .then_some(TestTimeOptions::new_from_env(false)),
+        extra_args: matches.opt_strs("kani-flag"),
     }
 }
 
@@ -292,7 +305,7 @@ pub fn test_opts(config: &Config) -> test::TestOpts {
         skip: vec![],
         list: false,
         options: test::Options::new(),
-        time_options: None,
+        time_options: config.time_opts,
         fail_fast: config.fail_fast,
         force_run_in_process: false,
     }
diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index 59b79a24d8d9..04647f7b6572 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -270,7 +270,8 @@ impl<'test> TestCx<'test> {
             .arg("kani")
             .arg("--target-dir")
             .arg(self.output_base_dir().join("target"))
-            .current_dir(&parent_dir);
+            .current_dir(&parent_dir)
+            .args(&self.config.extra_args);
         if test {
             cargo.arg("--tests");
         }