Support cvc5

[QDelta]

Rosette now supports boolector, z3 and cvc4, and cvc4 is succeeded by cvc5 now. So will rosette support cvc5? I notice that cvc4/cvc5 outperforms z3 in some cases, so it may be reasonable to support cvc5 for future improvements.

By just replacing the cvc4 executable with cvc5 I got an error:

read-solution: unrecognized solver output: #<eof>

It seems that they have different behaviors.

[sorawee]

The issue is that the cvc4 module in Rosette supplies the flag --bv-div-zero-const, which is supported in cvc4, but not in cvc5. If you manually remove the option in the cvc4 module, it should allow you to use cvc5 with the cvc4 module.

There's currently also an effort to add cvc5 to Rosette proper. See #260.

[sorawee]

Fixed by #260.