Adjust test patterns so as not to check for trivial properties (#3464)

With diffblue/cbmc#8413, CBMC will no longer create property checks for assigns clauses that are trivially true. We had CBMC-Nightly failing since August 17th given the CBMC change. This will bring CBMC-Nightly back to a passing state. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
model-checking · Aug 27, 2024 · d5c1b71 · d5c1b71
1 parent db9c45c
commit d5c1b71
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected
@@ -7,7 +7,7 @@ VERIFICATION:- SUCCESSFUL
 
 .assigns\
 - Status: SUCCESS\
-- Description: "Check that var_4 is assignable"\
+- Description: "Check that *dst is assignable"\
 in function copy
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected
@@ -7,7 +7,7 @@ VERIFICATION:- SUCCESSFUL
 
 copy.assigns\
 - Status: SUCCESS\
-- Description: "Check that var_5 is assignable"\
+- Description: "Check that *dst is assignable"\
 in function copy
 
 VERIFICATION:- SUCCESSFUL