Remove CVC4-only verification

AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

Apache License 2.0

106 stars 7 forks source link

Remove CVC4-only verification #247

Closed treiher closed 2 years ago

treiher commented 4 years ago

The CVC4-only verification tests almost always fail in our CI for no apparent reason. Neither an error message nor a log of the failing step is provided. We should disable those tests until we found a solution for this issue.

Alternative CI offerings:

senier commented 4 years ago

Is there a way to comment it out and add a comment pointing to a Workaround so we don't forget to re-enable it in the future?

treiher commented 4 years ago

Maybe. I would just keep this issue open until we find a solution. I think that is sufficient in this case.

senier commented 4 years ago

Then let's leave it open until the issue is fixed.

senier commented 2 years ago

Decision: Remove prove_tests_cvc4 make target in Makefile and prove_cvc4 in tests/spark/Makefile. This does not make sense right now as we don't have two provers which are able to reliably prove our code alone.