mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
cd4df2daff
This ensures that regressions pass when configuring in `safe-mode`. Note that *all* regression testers must now take into account whether we are in a safe-mode (safe mode itself is not a new tester). This makes the following changes: - `safe-mode: yes|no` is now an entry in `--show-config` - LibPoly and Cocoa are disabled by default when configuring with `safe-mode`. We give a warning if the user specified otherwise. - A few regressions are updated to have the appropriate options. - Option and logic exceptions that are "admissible" in safe mode are updated to contain the text `"in safe mode"`. - Various options that are used in run_regression.py are upgraded to "common" to ensure safe-mode is compatible with the tester. Removes a few unecessary options in run_regression.py. - Disables a number of unit tests and examples (in the CMake) that are not applicable in safe mode. - Adds a CI job to test a safe-mode build. Note that the CPC tester fails due to not guarding against some unsafe operators in the rewriter. I will address this in a separate PR.