Support for failing .smt and .smt2 regressions (and other examples with

Support for failing .smt and .smt2 regressions (and other examples with
additional output).  If the benchmark file has '% EXPECT: ' gestures,
like for cvc regressions, that is used (after being stripped out so that
the cvc4 smt parser never sees these special lines).  However, this can
be a pain, since then you can't run the regression manually on the
command line (since it fails to parse).  So if there is another file
in the same directory as $benchmark called $benchmark.expect, that is
scanned for '% EXPECT: ' etc., and the benchmark file is used verbatim.