Reduce CBMC verbosity to CBMC's default

CBMC v6 included changes to hide timing information and loop unwinding
status output at the default verbosity. To not impact Kani users, model-checking#2995
included changes to make Kani run CBMC with `--verbosity 9`. This change
now makes Kani run CBMC with just the default verbosity, hiding timing
information and loop unwinding status by default. If users still wish to
see this information, they can invoke Kani with
`--cbmc args --verbosity 9`.

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)
     }
 

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..."

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" ]

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`
 

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>`
 

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`
 

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
 

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
 

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)