Bella (Hydra v2.2.2)

Summary

Prepares for the upcoming CNF preprocessors (bipe) by restructuring the parser and integrating the preprocessing skeleton, and adds the option to set a random seed. Fixes two integer overflows, one on large formulae and one that caused an infinite loop on formulae of specific sizes.

Added

• Flag -seed to set the seed (randomly generated if omitted), which is printed to the console
• Seed in BellaTest (randomly generated if not provided), used for all tests and written to the log file

Refactored

• Restructured the parser in preparation for CNF preprocessors
• Handling of randomness

Fixed

• Integer overflow for formulae where the number of literals plus the number of clauses exceeds 2^32
• Infinite loop caused by an integer overflow for formulae where the number of variables is 2^8, 2^16, or 2^32 (or the number of literals is 2^8, 2^16, or 2^32), as encountered in [1]

Changed

• Standardised the exit codes using EXIT_SUCCESS and EXIT_FAILURE

Third-Party Software Updates

• unordered_dense: v4.9.1 → v5.3.1

[1] MENG, Qiaolan, et al. On Knowledge Compilation For Two-Variable First-Order Logic. arXiv preprint arXiv:2605.11796, 2026.