Remove CVC4-only verification

Open treiher opened this issue 5 years ago • 4 comments

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:

Azure Pipelines
Semaphore
Codefresh
CloudBees CodeShip

May 19 '20 08:05 treiher

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?

May 19 '20 09:05 senier

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

May 19 '20 09:05 treiher

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

May 19 '20 10:05 senier

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.

Aug 30 '22 13:08 senier