From 7829048b6db3e552ae1fda6a6c1975918c41f13b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 08:45:46 +0530 Subject: [PATCH] test: Make extent_separation.cpp's wrong copy write zeros, which the solver refutes at once. --- clang/test/Verify/suite/extent_separation.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/extent_separation.cpp b/clang/test/Verify/suite/extent_separation.cpp index 4219158d5d..19b811bed6 100644 --- a/clang/test/Verify/suite/extent_separation.cpp +++ b/clang/test/Verify/suite/extent_separation.cpp @@ -50,6 +50,9 @@ void copy(const int *a, int *out, int n) // VCR-NEXT: a // VCR-NEXT: post +// A copy that writes zeros: its invariant fails where a holds anything else, +// which the solver finds at once (a reversed copy took 30 to 60 s, and on a +// slow runner timed out). void wrong_copy(const int *a, int *out, int n) cppverify::pre(n >= 0 && valid(a, n) && valid(out, n)) cppverify::modifies(*out) @@ -61,7 +64,7 @@ void wrong_copy(const int *a, int *out, int n) cppverify::invariant(cppverify::forall(j, 0, i, out[j] == a[j])) cppverify::decreases(n - i) { - out[i] = a[n - 1 - i]; + out[i] = 0; i = i + 1; } }