CVC4 backend doesn't work for --smt-formula-(only|too)

[fbrausse]

Unfortunately, the cvc4 backend can't produce SMT output files right now

Originally posted by @fbrausse in #1829 (comment)

Here is the reason:

esbmc/src/solvers/cvc4/cvc_conv.cpp

Line 1280 in 834ea81

log_debug("cvc4", "{}", oss.str());

[lucasccordeiro]

@rafaelsamenezes was working on the integration of CVC5 into ESBMC.

@rafaelsamenezes: can I ask you for the status?

[fbrausse]

@lucasccordeiro I believe it's waiting for me to check the floating point API usage of cvc5. I'll take a look...

[lucasccordeiro]

Yes.

Yesterday, @rafaelsamenezes told me that it would be great if you could check the FP API before proceeding with this integration.