diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index a0be50ab0428..387a9723fcdb 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -153,6 +153,11 @@ 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 170ef7682e3b..a7e2710773aa 100755
--- a/scripts/kani-perf.sh
+++ b/scripts/kani-perf.sh
@@ -27,8 +27,7 @@ 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 \
-  --kani-flag="--enable-unstable" --kani-flag="--cbmc-args" --kani-flag="--verbosity" --kani-flag="9"
+cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast
 exit_code=$?
 
 echo "Cleaning up..."
diff --git a/tests/cargo-kani/simple-kissat/Cargo.toml b/tests/cargo-kani/simple-kissat/Cargo.toml
index 260c3f62313c..3bde94c619fb 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", "--verbosity", "9" ]
+cbmc-args = ["--external-sat-solver", "kissat" ]
diff --git a/tests/ui/solver-attribute/cadical/test.rs b/tests/ui/solver-attribute/cadical/test.rs
index 2c4feaa4c356..d8e897f923fb 100644
--- a/tests/ui/solver-attribute/cadical/test.rs
+++ b/tests/ui/solver-attribute/cadical/test.rs
@@ -1,6 +1,5 @@
 // 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 c79618ecd028..3529deb0eea9 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 --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver bin=kissat
 
 //! 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 8742c1e2df87..a7b6e1304bf3 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 --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver cadical
 
 //! 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 4d876cdb952f..0b1403132ae3 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 --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver kissat
 
 //! 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 44778fd4f704..b92a4cd1b6c6 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 --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver minisat
 
 //! Checks that `--solver minisat` is accepted
 
diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py
index 124e16b2ceb7..ccf2259f7f0b 100644
--- a/tools/benchcomp/test/test_regression.py
+++ b/tools/benchcomp/test/test_regression.py
@@ -56,8 +56,7 @@ 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 "
-            "--enable-unstable --cbmc-args --verbosity 9 > "
+            "kani tests/kani/Unwind-Attribute/fixme_lib.rs > "
             "build/tests/perf/Unwind-Attribute/expected/expected.out"
         )
         self._run_kani_perf_test(cmd, False)
@@ -66,8 +65,7 @@ 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 "
-            "--enable-unstable --cbmc-args --verbosity 9 > "
+            "kani tests/kani/Arbitrary/arbitrary_impls.rs > "
             "build/tests/perf/Arbitrary/expected/expected.out"
         )
         self._run_kani_perf_test(cmd, True)