Adjust test patterns so as not to check for trivial properties

With diffblue/cbmc#8413, CBMC will no longer create property checks for assigns clauses that are trivially true.
tautschnig · Aug 27, 2024 · 8814d67 · 8814d67
1 parent db9c45c
commit 8814d67
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