diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 387a9723fcdb..a0be50ab0428 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -153,11 +153,6 @@ impl KaniSession {
 
         args.push(file.to_owned().into_os_string());
 
-        // Make CBMC verbose by default to tell users about unwinding progress. This should be
-        // reviewed as CBMC's verbosity defaults evolve.
-        args.push("--verbosity".into());
-        args.push("9".into());
-
         Ok(args)
     }
 
diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh
index a7e2710773aa..170ef7682e3b 100755
--- a/scripts/kani-perf.sh
+++ b/scripts/kani-perf.sh
@@ -27,7 +27,8 @@ done
 suite="perf"
 mode="cargo-kani-test"
 echo "Check compiletest suite=$suite mode=$mode"
-cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast
+cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast \
+  --kani-flag="--enable-unstable" --kani-flag="--cbmc-args" --kani-flag="--verbosity" --kani-flag="9"
 exit_code=$?
 
 echo "Cleaning up..."
diff --git a/tests/cargo-kani/simple-kissat/Cargo.toml b/tests/cargo-kani/simple-kissat/Cargo.toml
index 3bde94c619fb..260c3f62313c 100644
--- a/tests/cargo-kani/simple-kissat/Cargo.toml
+++ b/tests/cargo-kani/simple-kissat/Cargo.toml
@@ -12,4 +12,4 @@ description = "Tests that Kani can be invoked with Kissat"
 
 [kani.flags]
 enable-unstable = true
-cbmc-args = ["--external-sat-solver", "kissat" ]
+cbmc-args = ["--external-sat-solver", "kissat", "--verbosity", "9" ]
diff --git a/tests/ui/solver-attribute/cadical/test.rs b/tests/ui/solver-attribute/cadical/test.rs
index d8e897f923fb..2c4feaa4c356 100644
--- a/tests/ui/solver-attribute/cadical/test.rs
+++ b/tests/ui/solver-attribute/cadical/test.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that `cadical` is a valid argument to `kani::solver`
 
diff --git a/tests/ui/solver-option/bin/test.rs b/tests/ui/solver-option/bin/test.rs
index 3529deb0eea9..c79618ecd028 100644
--- a/tests/ui/solver-option/bin/test.rs
+++ b/tests/ui/solver-option/bin/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver bin=kissat
+// kani-flags: --solver bin=kissat --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that `--solver` accepts `bin=<binary>`
 
diff --git a/tests/ui/solver-option/cadical/test.rs b/tests/ui/solver-option/cadical/test.rs
index a7b6e1304bf3..8742c1e2df87 100644
--- a/tests/ui/solver-option/cadical/test.rs
+++ b/tests/ui/solver-option/cadical/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver cadical
+// kani-flags: --solver cadical --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that the `cadical` is supported as an argument to `--solver`
 
diff --git a/tests/ui/solver-option/kissat/test.rs b/tests/ui/solver-option/kissat/test.rs
index 0b1403132ae3..4d876cdb952f 100644
--- a/tests/ui/solver-option/kissat/test.rs
+++ b/tests/ui/solver-option/kissat/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver kissat
+// kani-flags: --solver kissat --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that the solver option overrides the solver attribute
 
diff --git a/tests/ui/solver-option/minisat/test.rs b/tests/ui/solver-option/minisat/test.rs
index b92a4cd1b6c6..44778fd4f704 100644
--- a/tests/ui/solver-option/minisat/test.rs
+++ b/tests/ui/solver-option/minisat/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver minisat
+// kani-flags: --solver minisat --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that `--solver minisat` is accepted
 
diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py
index ccf2259f7f0b..124e16b2ceb7 100644
--- a/tools/benchcomp/test/test_regression.py
+++ b/tools/benchcomp/test/test_regression.py
@@ -56,7 +56,8 @@ def test_kani_perf_fail(self):
         cmd = (
             "rm -rf build target &&"
             "mkdir -p build/tests/perf/Unwind-Attribute/expected &&"
-            "kani tests/kani/Unwind-Attribute/fixme_lib.rs > "
+            "kani tests/kani/Unwind-Attribute/fixme_lib.rs "
+            "--enable-unstable --cbmc-args --verbosity 9 > "
             "build/tests/perf/Unwind-Attribute/expected/expected.out"
         )
         self._run_kani_perf_test(cmd, False)
@@ -65,7 +66,8 @@ def test_kani_perf_success(self):
         cmd = (
             "rm -rf build target &&"
             "mkdir -p build/tests/perf/Arbitrary/expected &&"
-            "kani tests/kani/Arbitrary/arbitrary_impls.rs > "
+            "kani tests/kani/Arbitrary/arbitrary_impls.rs "
+            "--enable-unstable --cbmc-args --verbosity 9 > "
             "build/tests/perf/Arbitrary/expected/expected.out"
         )
         self._run_kani_perf_test(cmd, True)