[SwayamInSync]

Three tests fail on CI runners for reasons outside the code they test. Both block every PR, since each PR's checks run on its merge with main.

cvc5_memory_limit.cpp under cvc5 1.4.2

The test is from #48. It fails in the assertions job since #100 put cvc5 1.4.2 there (#94's run printed Verified: small [backend=cvc5] where the test expects solver.memory-limit).

The test gives each cvc5 process 5 MB of data (--memory-limit=5, RLIMIT_DATA), assuming cvc5 cannot solve the query within that. cvc5 1.1.2 cannot, but 1.4.2 solves it in less. Here is the overflow check's query, as cpp-verify --dump-smt2 writes it, run under prlimit --data=N:

limit	cvc5 1.1.2	cvc5 1.4.2
5 MB	terminated by the C++ runtime	unsat
2 MB		segfault
1 MB	(error "std::bad_alloc")	(error "std::bad_alloc")

The limit works; only the test's assumption about cvc5's footprint fails for 1.4.2.

1 MB was not the fix. A first version gave 1 MB, which Ubuntu's cvc5 1.1.2 and the static 1.4.2 both answered with std::bad_alloc here. In CI, the release job's cvc5 is the static 1.1.2 archive, and it segfaulted at 1 MB (cvc5 terminated by signal 11: cvc5 suffered a segfault ... Looks like a NULL pointer was dereferenced.). An allocation that fails where cvc5 does not check it crashes it, and where that happens depends on the limit, the version, and the build. With the test's old query:

limit	Ubuntu cvc5 1.1.2	static cvc5 1.4.2
1 MB	out of memory	out of memory
2 MB	out of memory	segfault
3 MB	out of memory	exit status 1
4, 5 MB	out of memory	Verified
6 MB	segfault	Verified

So the test no longer sits among cvc5's start-up allocations. Its function multiplies three 64-bit values, which cvc5 bit-blasts, and the limit is 16 MB: each version starts, then runs out while solving, where its allocations throw. Ubuntu's 1.1.2 and the static 1.4.2 each pass three runs of three, out of memory after 0.6 to 0.9 s; at 16 and 32 MB both report solver.memory-limit, and without a limit the query runs for a minute.

A cvc5 that crashes is still reported as a failed invocation, not as running out of memory, since a crash need not mean that. One crash does say so: GMP aborts with GNU MP: Cannot allocate memory, which cpp-verify reports as a failed invocation today; recognizing it, as Why3's prover drivers do, is a change of its own.

spec_post_unfolded.cpp on a slow core

fibo_strict failed #87's macOS job three times out of three (Unresolved: fibo_strict [backend=z3] [reason=spec.fuel] where the test expects a certified counterexample). #87 does not cause it: its Layer-3 dump of this file is byte-identical with and without #87.

The counterexample (fibo(-2) == fibo(-1) == 0) is found by refinement and by the search for the ends of a domain. Both get a slice of wall-clock time: 5% of --timeout, at least 500 ms, which is 500 ms at the test's --timeout=10000. Here, with cpp-verify on one core shared with two busy loops (taskset -c 7), the slice runs out before the counterexample is found:

--timeout	runs	fibo_strict
10000 (500 ms slice)	8	spec.fuel 3 times, the counterexample 5 times
40000 (2 s slice)	8	the counterexample 8 times, 5.5 s each

Verdicts may depend on load (wall-clock budgets stay, decision C1), so the test gets a budget its slice survives on: --timeout=40000. On an idle machine the file takes 2.2 s either way, and every check of the file passes with the new budget.

extent_separation.cpp on a slow core

extent_separation.cpp failed on #93's macOS runner, a change that touches no verifier code:

extent_separation.cpp:61:26: Unresolved: wrong_copy [backend=z3] [reason=solver.timeout] (proof obligation ...::invariant-preserved@...)
Summary: 7 verified, 2 failed, 1 unresolved (solver.timeout 1) in 61.1 s

wrong_copy is the test's negative case: a copy loop that writes the wrong values must fail its invariant. It wrote a[n - 1 - i], a reversed copy, and finding a counterexample to its quantified invariant is a hard search. On a Linux machine, three runs of wrong_copy alone with --jobs=1 took 32.6 s and 41.9 s to fail, and the third ended Unresolved [solver.timeout] after 61.5 s.

The loop now writes zeros (out[i] = 0;). The invariant out[j] == a[j] then fails wherever a holds another value: three runs failed in 1.4 s each, and the whole file takes 0.7 s. The case still shows what it is for: under the separation of extents, a copy that is wrong fails, and copy verifies.

This was #112, moved here so that one CI run covers all three; together they unblock the stack #93 to #99, whose assertions jobs fail only on cvc5_memory_limit.cpp and whose macOS job failed on this test.