diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index cc13306a4eaf..81253f1a9790 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -47,7 +47,7 @@ jobs: - name: 'Run Clippy' run: | - cargo clippy --all -- -D warnings + cargo clippy --workspace --exclude charon --exclude macros --no-deps -- -D warnings - name: 'Print Clippy Statistics' run: | diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 8c61173bae0e..b32b2e3a52a7 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -636,16 +636,15 @@ impl ValidateArgs for VerificationArgs { )); } - if self.common_args.unstable_features.contains(UnstableFeature::Aeneas) { - if !self.cbmc_args.is_empty() { - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "The `--cbmc-args` argument cannot be used with -Z aeneas.", - )); - } - // TODO: error out for other CBMC-backend-specific arguments + // TODO: error out for other CBMC-backend-specific arguments + if self.common_args.unstable_features.contains(UnstableFeature::Aeneas) + && !self.cbmc_args.is_empty() + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The `--cbmc-args` argument cannot be used with -Z aeneas.", + )); } - Ok(()) } }