--rewrite-divk for CVC4

By default, CVC4 cannot handle division in linear integer arithmetic logics like
QF_LIA (what Rumur speaks by default). The option --rewrite-divk makes it try a
work around for division by constants or other manageable quantities by
rewriting division into other operations.

It's still not capable of handling the full expression space of division, but I
don't think we should bail out on encountering an unsupported division
expression because other SMT solvers like Z3 can manage these. For now an
unsupported division expression results in a failing call to CVC4. However, the
failure is invisible unless you pass --debug.