Remove remaining --enable-unstable mentions

.github/workflows/verify-std-check.yml

@@ -59,7 +59,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
+            -Z mem-predicates -Z loop-contracts --cbmc-args --object-bits 12
 
       # If the head failed, check if it's a new failure.
       - name: Checkout BASE
@@ -89,7 +89,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
+            -Z mem-predicates -Z loop-contracts --cbmc-args --object-bits 12
 
       - name: Compare PR results
         if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome

docs/src/reference/experimental/stubbing.md

@@ -16,8 +16,7 @@ Although definitions for *mocking* (normally used in testing) and *stubbing* may
 
 ## Components
 
-The stubbing feature can be enabled by using the `--enable-stubbing` option when calling Kani.
-Since it's an unstable feature, it requires passing the `--enable-unstable` option in addition to `--enable-stubbing`.
+The stubbing feature can be enabled by using the `-Z stubbing` option when calling Kani (the `-Z` indicates that it's an unstable feature).
 
 At present, the only component of the stubbing feature is [the `#[kani::stub(<original>, <replacement>)]` attribute](#the-kanistub-attribute),
 which allows you to specify the pair of functions/methods that must be stubbed in a harness.
@@ -60,6 +59,8 @@ At present, Kani fails to verify this example due to [issue #1781](https://githu
 However, we can work around this limitation thanks to the stubbing feature:
 
 ```rust
+use rand::random;
+
 #[cfg(kani)]
 fn mock_random<T: kani::Arbitrary>() -> T {
     kani::any()
@@ -83,7 +84,8 @@ Note that this is a fair assumption to do: `rand::random` is expected to return
 Now, let's run it through Kani:
 
 ```bash
-cargo kani --enable-unstable --enable-stubbing --harness encrypt_then_decrypt_is_identity
+cargo add rand
+cargo kani -Z stubbing --harness encrypt_then_decrypt_is_identity
 ```
 
 The verification result is composed of a single check: the assertion corresponding to `assert_eq!(data, decrypted_data)`.

docs/src/usage.md

@@ -23,7 +23,7 @@ This works like `cargo test` except that it will analyze all proof harnesses ins
 
 Common to both `kani` and `cargo kani` are many command-line flags:
 
- * `--concrete-playback=[print|inplace]`: _Experimental_, `--enable-unstable` feature that generates a Rust unit test case
+ * `--concrete-playback=[print|inplace]`: _Experimental_ feature that generates a Rust unit test case
  that plays back a failing proof harness using a concrete counterexample.
  If used with `print`, Kani will only print the unit test to stdout.
  If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [concrete playback](./experimental/concrete-playback.md) section.

tests/script-based-pre/check-output/check-output.sh

@@ -31,7 +31,7 @@ cd $(dirname $0)
 
 echo "Running single-file check..."
 rm -rf *.c
-kani --gen-c --enable-unstable singlefile.rs >& kani.log || \
+kani --gen-c -Z unstable-options singlefile.rs >& kani.log || \
     { ret=$?; echo "== Failed to run Kani"; cat kani.log; rm kani.log; exit 1; }
 rm -f kani.log
 if ! [ -e singlefile_*main.c ]
@@ -70,7 +70,7 @@ echo
 (cd multifile
 echo "Running multi-file check..."
 rm -rf build
-cargo kani --target-dir build --gen-c --enable-unstable >& kani.log || \
+cargo kani --target-dir build --gen-c -Z unstable-options >& kani.log || \
     { ret=$?; echo "== Failed to run Kani"; cat kani.log; rm kani.log; exit 1; }
 rm -f kani.log
 cd build/kani/${TARGET}/debug/deps/

tests/ui/cbmc_checks/float-overflow/check_message.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --cbmc-args --float-overflow-check
+// kani-flags: -Z unstable-options --cbmc-args --float-overflow-check
 // Check we don't print temporary variables as part of CBMC messages.
 extern crate kani;