forgot to copy paste test in

model-checking · Jun 28, 2024 · b28f752 · b28f752
1 parent 1d1cbf7
commit b28f752
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/tests/ui/function-contracts/mutating_ensures_error.rs b/tests/ui/function-contracts/mutating_ensures_error.rs
@@ -1 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|_| {*_x += 1; true})]
+fn unit(_x: &mut u32) {
+}
+
+#[kani::proof_for_contract(id)]
+fn harness() {
+    let mut x = kani::any();
+    unit(&mut x);
+}