Minisat ran out of memory

[mereolog]

Running the following command with Vampire 4.9:
./vampire --saturation_algorithm fmb -t 0 -m 1000000 bfo.tptp > bfo.szs
I got a 'Minisat ran out of memory' error - see below.

Note that the VM I use has 1TB of RAM, so the source does not seem to be related to the hardware limits.

Here is the input file: bfo.tptp.zip

% Running in auto input_syntax mode. Trying TPTP
Detected minimum model sizes of [35]
Detected maximum model sizes of [max]
TRYING [35]
Minisat ran out of memory
% ------------------------------
% Version: Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)
% Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d
% Termination reason: Unknown
% Termination phase: Finite model building constraint generation

% Memory used [KB]: 394148089
% Time elapsed: 1626.808 s
% ------------------------------
% ------------------------------
Version : Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)

[quickbeam123]

Dear @mereolog, what you describe does not sound like an obvious bug. Minisat has it own memory management embedded in vampire's, and the "Minisat ran out of memory" message is a possible way of ending an fmb attempt.

I you are hinting at the "% Memory used" statistics not reaching quite all the way to 1TB yet, this has been changed in the more recent version (so the old code, which was a bit rusty anyway, is no longer supported). If you would like to try with the most recent master version of Vampire, I would be curious what you will see. The new statistic is "Peak memory usage: " and relies on the getrusage / usage.ru_maxrss system call.