[SwayamInSync]

Under --memory-limit, cvc5 can stop in three ways when an allocation fails. Two were reported as running out of memory; GMP's was not:

$ cpp-verify --backend=cvc5 --memory-limit=5 seqs.cpp      # cvc5 1.4.2, static
... [reason=solver.invocation-failed] (... cvc5 exited with status -2: cvc5 terminated by signal 6: GNU MP: Cannot allocate memory (size=8))

GMP, cvc5's arithmetic library, calls abort with that message when its allocator returns nothing. The message says why the solver stopped, as std::bad_alloc and the SAT solver's OutOfMemoryException do, so it now gives solver.memory-limit. This matches Why3's prover drivers, which read a prover's out-of-memory from its output (outofmemory patterns), as Frama-C's WP reports it.

A crash with no such message stays solver.invocation-failed: cvc5 also segfaults where it dereferences an allocation it did not check, but a segfault need not come from memory. The tooling page now says so. #106 found these crashes: at a few megabytes they happen at limits that differ between versions and builds.

Tests

solver_portfolio_process.test runs a fake cvc5 (Inputs/fake_cvc5.py, mode gmp) that prints GMP's message and aborts, and expects solver.memory-limit with the limit named; its existing crash mode still expects solver.invocation-failed. On the base the new check fails: the fake gives solver.invocation-failed (... terminated by signal 6: GNU MP: Cannot allocate memory (size=8)).

Docs

Tooling (how cvc5 stops at the limit, and that a crash is no proof of it) and release notes.