add simple precedence test

tests/expected/function-contract/as-assertions/precedence.expected

@@ -1,3 +1,12 @@
+
+assertion\
+	 - Status: SUCCESS\
+	 - Description: "attempt to add with overflow"
+
+assertion\
+	 - Status: SUCCESS\
+	 - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr"
+
 assertion\
 	 - Status: UNREACHABLE\
 	 - Description: "*add_one_ptr == 4"
@@ -22,4 +31,4 @@ assertion\
 	 - Status: SUCCESS\
 	 - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr"
 
-Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Complete - 3 successfully verified harnesses, 0 failures, 3 total.

tests/expected/function-contract/as-assertions/precedence.rs

@@ -26,16 +26,25 @@ fn add_one(add_one_ptr: &mut u32) {
     *add_one_ptr += 1;
 }
 
-// Test that proof_for_contract takes precedence over the assert mode, i.e.
-// that the target of the proof for contract still has its preconditions assumed
+// Simple test that proof_for_contract takes precedence over the assert mode, i.e.
+// that the target of the proof for contract still has its preconditions assumed.
+// If the precondition wasn't assumed, then the addition would overflow,
+// so if verification succeeds, we know that the precondition was assumed.
+#[kani::proof_for_contract(add_one)]
+fn simple_proof_for_contract_takes_precedence() {
+    let mut i = kani::any();
+    add_one(&mut i);
+}
+
+// Complex test that proof_for_contract takes precedence over the assert mode
 // when combined with other contracts that are being asserted.
 // In this harness, add_three and add_two's contracts are asserted, but add_one (the target) should have its precondition assumed.
 // So, assume add_three's precondition to ensure that its precondition assertion passes,
 // but do not assume add_one's stricter precondition--if precedence is implemented correctly
 // it should get assumed without us having to specify it in the harness, and verification should succeed.
 // For a version of this harness without the assumption, see assert-preconditions::prove_add_one.
 #[kani::proof_for_contract(add_one)]
-fn proof_for_contract_takes_precedence() {
+fn complex_proof_for_contract_takes_precedence() {
     let mut i = kani::any();
     kani::assume(i < 100);
     add_three(&mut i);