test: three tests that failed on CI runners (cvc5 1.1.2 and 1.4.2, slow macOS cores)

clang/test/Verify/suite/cvc5_memory_limit.cpp

@@ -1,16 +1,19 @@
 // REQUIRES: cvc5, system-linux
-// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=5 %s -- 2>&1 \
+// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=16 %s -- 2>&1 \
 // RUN:   | FileCheck %s
 //
 // Each cvc5 process may allocate --memory-limit megabytes; on Linux that is
-// its data (RLIMIT_DATA). cvc5 needs more than 5 to start solving, so every
-// query runs out, which cvc5 reports as std::bad_alloc or as its SAT solver's
-// OutOfMemoryException.
+// its data (RLIMIT_DATA). Bit-blasting these 64-bit products needs far more
+// than 16, so every query runs out once it is solving, which cvc5 reports as
+// std::bad_alloc or as its SAT solver's OutOfMemoryException. At a few
+// megabytes cvc5 may instead crash where an allocation fails, at limits that
+// differ between versions and builds (1.1.2 at 1 and 6, 1.4.2 at 2 and 3),
+// and 1.4.2 solves a small query within 4.
 
-int small(int x)
-  cppverify::pre(x < 100)
-  cppverify::post(cppverify::result == x + 1)
+unsigned long long mix(unsigned long long a, unsigned long long b,
+                       unsigned long long c)
+  cppverify::post(cppverify::result == (a ^ b) * (b ^ c) * (c ^ a))
 {
-  return x + 1;
+  return (a ^ b) * (b ^ c) * (c ^ a);
 }
-// CHECK: Unresolved: small [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 5 MB (--memory-limit))
+// CHECK: Unresolved: mix [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 16 MB (--memory-limit))

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;
   }
 }

clang/test/Verify/suite/spec_post_unfolded.cpp

@@ -1,4 +1,4 @@
-// RUN: not %cpp-verify --timeout=10000 %s -- 2>&1 | FileCheck %s
+// RUN: not %cpp-verify --timeout=40000 %s -- 2>&1 | FileCheck %s
 // RUN: %cpp-verify --lower-only --dump-ir=4 %s -- 2>&1 | FileCheck %s --check-prefix=DUMP
 //
 // A spec's proved postcondition holds at every application the solver sees,
@@ -30,7 +30,10 @@ cppverify::proof void fibo_monotone(int i, int j)
 // DUMP: (>= (spec${{[^ ]+}} (- j_0 2)) 0)
 
 // The facts are theorems, so a false claim still fails with a certified
-// counterexample: fibo(-2) == fibo(-1) == 0.
+// counterexample: fibo(-2) == fibo(-1) == 0. Refinement and the search for
+// the ends of a domain, which find it, get 5% of --timeout, at least 500 ms;
+// on a slow or busy core (macOS runners, or one core shared with two busy
+// loops) 500 ms was too little in 2 of 4 runs, and the RUN line gives 2 s.
 cppverify::proof void fibo_strict(int i, int j)
   cppverify::pre(i < j)
   cppverify::post(fibo(i) < fibo(j))