CVC5 works only with batch mode

[atomb]

This doesn't work:

$ boogie -proverOpt:SOLVER=cvc5 -timeLimit:10 Test/textbook/DutchFlag.bpl
<hangs>

Similar behavior comes up with most Boogie inputs. This is just a representative example.

This finishes in less than a second:

$ boogie -proverOpt:SOLVER=cvc5 -timeLimit:10 -proverOpt:BATCH_MODE=true Test/textbook/DutchFlag.bpl
Boogie program verifier finished with 1 verified, 0 errors

[shazqadeer]

@atomb :

What does BATCH_MODE do for CVC5?

Is the problem only for this program or is BATCH_MODE required for any Boogie program to verify with CVC5?

[atomb]

Batch mode is the opposite of incremental mode. That is, each query is entirely self-contained with no (push) or (pop) commands, for use with provers that don't support incremental queries (though it's also entirely possible to use it with provers that do support incremental queries, too).

In principle, CVC5 should work with the incremental interface, but something is going wrong. It could have to do with the ping/pong stuff used to determine whether the solver is still alive.

I think it affects most programs, not just the one above.

And, just to be clear, I'm not filing this to put any more work on anyone else's plate. I plan to investigate it and fix it myself.