Reduce CBMC verbosity to CBMC's default

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)