Add tests

Author: tautschnig

tests/kani/StdOverrides/align_offset.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test makes sure Kani uses its hook for align_offset.
+
+#[kani::proof]
+fn align_offset() {
+    let x = 10;
+    let ptr = &x as *const i32;
+    let alignment = ptr.align_offset(1);
+    assert_eq!(alignment, usize::MAX);
+}

tests/kani/Strings/2363.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test is to check that we have addressed the performance issue called out in
+//! https://github.com/model-checking/kani/issues/2363.
+
+#[kani::proof]
+#[kani::unwind(7)]
+#[kani::solver(cadical)]
+fn main() {
+    let s = "Mary had a little lamb";
+    let v: Vec<&str> = s.split(' ').collect();
+    assert_eq!(v, ["Mary", "had", "a", "little", "lamb"]);
+}