slice-formula is enabled unconditionally, but should not be used when getting traces

[tedinski]

CBMC's --slice-formula can result in bizarre traces with weird values being assigned to variables CBMC no longer considers important.

We should not enable it when we're generating traces.

We should also have a flag that allows disabling it (--no-slice-formula?)