You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
What is wrong
Currently, regression tests rely on both Minisat and SPASS. The regression test suite thus reports 8 total failures when run on a freshly cloned repository:
2 reported failures are from book code examples that are meant to raise errors.
1 reported failure is due to proof search failing when using a build generated by SML/NJ. This failure is not due to problems with Athena, rather, the non-deterministic nature of proof search procedures, possible timeouts, etc.
1 reported failure is due to missing the minisat_out.txt file in the ATHENA_HOME directory.
The other four failures are due to external calls to either Minisat or SPASS, which fail when they have not been installed.
How to fix
First, we will remove the intentionally incorrect code examples since they are meant for pedagogical purposes. Later, we might add to the python regression script an ability to expect an error from the Athena proof-checking.
Next, we will add to the regression testing script(s) an initial procedure that checks for Minisat and SPASS in the user's path. If Minisat is present, the original tests will be used, otherwise, it will trigger equivalent tests that use an Athena-native sat procedure. If SPASS is absent, tests that rely on SPASS will simply be skipped.
The text was updated successfully, but these errors were encountered:
What is wrong
Currently, regression tests rely on both Minisat and SPASS. The regression test suite thus reports 8 total failures when run on a freshly cloned repository:
2 reported failures are from
book
code examples that are meant to raise errors.1 reported failure is due to proof search failing when using a build generated by SML/NJ. This failure is not due to problems with Athena, rather, the non-deterministic nature of proof search procedures, possible timeouts, etc.
1 reported failure is due to missing the
minisat_out.txt
file in theATHENA_HOME
directory.The other four failures are due to external calls to either Minisat or SPASS, which fail when they have not been installed.
How to fix
First, we will remove the intentionally incorrect code examples since they are meant for pedagogical purposes. Later, we might add to the python regression script an ability to expect an error from the Athena proof-checking.
Next, we will add to the regression testing script(s) an initial procedure that checks for Minisat and SPASS in the user's path. If Minisat is present, the original tests will be used, otherwise, it will trigger equivalent tests that use an Athena-native
sat
procedure. If SPASS is absent, tests that rely on SPASS will simply be skipped.The text was updated successfully, but these errors were encountered: