Address PR comments

zhassan-aws · Sep 27, 2024 · eac417a · eac417a
1 parent 9294590
commit eac417a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -1,5 +1,7 @@
-// Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
 
 //! This module contains a context for translating stable MIR into Charon's
 //! unstructured low-level borrow calculus (ULLBC)

diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
@@ -55,8 +55,6 @@ impl KaniSession {
         kani_args.push(format!("--reachability={}", self.reachability_mode()));
         if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) {
             kani_args.push("--backend=aeneas".into());
-        } else {
-            kani_args.push("--backend=cprover".into());
         }
 
         let lib_path = lib_folder().unwrap();