Upgrade Rust toolchain to 2025-09-19

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -1437,7 +1437,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 };
                 CharonTy::new(CharonTyKind::Arrow(rb))
             }
-            RigidTy::Dynamic(_, _, _) => {
+            RigidTy::Dynamic(_, _) => {
                 CharonTy::new(CharonTyKind::DynTrait(CharonExistentialPredicate))
             }
             _ => todo!("Not yet implemented RigidTy: {:?}", rigid_ty),

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -1145,7 +1145,7 @@ impl GotocCtx<'_, '_> {
                 match dst_subt.kind() {
                     TyKind::RigidTy(RigidTy::Slice(_))
                     | TyKind::RigidTy(RigidTy::Str)
-                    | TyKind::RigidTy(RigidTy::Dynamic(_, _, _)) => {
+                    | TyKind::RigidTy(RigidTy::Dynamic(_, _)) => {
                         //TODO: this does the wrong thing on Strings/fixme_boxed_str.rs
                         // if we cast to slice or string, then we know the source is also a slice or string,
                         // so there shouldn't be anything to do

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -25,7 +25,7 @@ use rustc_public::mir::Body;
 use rustc_public::mir::mono::Instance as InstanceStable;
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
-    Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
+    Binder, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
     Ty as StableTy,
 };
 use rustc_span::def_id::DefId;
@@ -301,8 +301,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
         predictates.extend(
             projections.into_iter().map(|proj| proj.map_bound(ExistentialPredicate::Projection)),
         );
-        let rigid =
-            RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }, DynKind::Dyn);
+        let rigid = RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased });
 
         rustc_public::ty::Ty::from_rigid_kind(rigid)
     }
@@ -419,7 +418,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
     /// We follow the order from the `TyCtxt::COMMON_VTABLE_ENTRIES`.
     fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec<DatatypeComponent> {
         let mut vtable_base = common_vtable_fields(self.trait_vtable_drop_type(t));
-        if let ty::Dynamic(binder, _, _) = t.kind() {
+        if let ty::Dynamic(binder, _) = t.kind() {
             // The virtual methods on the trait ref. Some auto traits have no methods.
             if let Some(principal) = binder.principal() {
                 let poly = principal.with_self_ty(self.tcx, t);

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs

@@ -418,7 +418,7 @@ impl MirVisitor for CheckUninitVisitor {
                     .rigid()
                     .expect("should be working with monomorphized code")
                 {
-                    RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => {
+                    RigidTy::Adt(..) | RigidTy::Dynamic(_, _) => {
                         self.push_target(MemoryInitOp::SetRef {
                             operand: Operand::Copy(place.clone()),
                             value: true,

kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs

@@ -398,7 +398,7 @@ fn data_bytes_for_ty(
                 | RigidTy::CoroutineClosure(_, _)
                 | RigidTy::CoroutineWitness(_, _)
                 | RigidTy::Foreign(_)
-                | RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)),
+                | RigidTy::Dynamic(_, _) => Err(LayoutComputationError::UnsupportedType(ty)),
             }
         }
         FieldsShape::Union(_) => Err(LayoutComputationError::UnionAsField(ty)),

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -1061,7 +1061,7 @@ pub fn ty_validity_per_offset(
                 | RigidTy::CoroutineClosure(_, _)
                 | RigidTy::CoroutineWitness(_, _)
                 | RigidTy::Foreign(_)
-                | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")),
+                | RigidTy::Dynamic(_, _) => Err(format!("Unsupported {ty:?}")),
             }
         }
         FieldsShape::Union(_) | FieldsShape::Array { .. } => {

kani-driver/src/call_cbmc.rs

@@ -145,27 +145,24 @@ impl KaniSession {
             .await)
         };
 
-        let verification_results = if res.is_err() {
+        if let Ok(output) = res {
+            // The timeout wasn't reached
+            Ok(VerificationResult::from(output?, harness.attributes.should_panic, start_time))
+        } else {
             // An error occurs if the timeout was reached
 
             // Kill the process
             cbmc_process.kill().await?;
 
-            VerificationResult {
+            Ok(VerificationResult {
                 status: VerificationStatus::Failure,
                 failed_properties: FailedProperties::None,
                 results: Err(ExitStatus::Timeout),
                 runtime: start_time.elapsed(),
                 generated_concrete_test: false,
                 coverage_results: None,
-            }
-        } else {
-            // The timeout wasn't reached
-            let output = res.unwrap()?;
-            VerificationResult::from(output, harness.attributes.should_panic, start_time)
-        };
-
-        Ok(verification_results)
+            })
+        }
     }
 
     /// "Internal," but also used by call_cbmc_viewer

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-09-18"
+channel = "nightly-2025-09-19"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]