Improve performance for align offset harness (model-checking#89)

Currently, this harness takes 21 minutes in CI. The only point of this
harness is to verify the contract for pointee types with a non-power of
two byte size--17 was an arbitrary choice. Reducing to 5 and changing
the solver reduces verification time to 57 seconds on my local machine.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: carolynzech

library/core/src/ptr/mod.rs

@@ -2552,8 +2552,12 @@ mod verify {
     }
 
     #[kani::proof_for_contract(align_offset)]
-    fn check_align_offset_17() {
-        let p = kani::any::<usize>() as *const [char; 17];
+    // 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];
         check_align_offset(p);
     }