CVC4 1.7 has some strange behavior when invoked with --string-exp,
therefore by default it is not invoked with this flag. Why3 string
theory is used instead of built-in CVC4 string theory.

Alternative prover that invokes CVC4 1.7 with --string-exp and uses
the built-in string theory is now provided.