add explanatory comment

model-checking · Sep 19, 2024 · d0abafc · d0abafc
1 parent 7707ea5
commit d0abafc
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
@@ -2552,6 +2552,9 @@ mod verify {
     }
 
     #[kani::proof_for_contract(align_offset)]
+    // The purpose of this harness is to test align_offset with a pointee type whose stride is not a power of two
+    // Keeping the size smaller (5) and changing the solver to kissat improves verification time
+    // c.f. https://github.com/model-checking/verify-rust-std/pull/89
     #[kani::solver(kissat)]
     fn check_align_offset_5() {
         let p = kani::any::<usize>() as *const [char; 5];