By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1

and SMT-LIBv2).

There are --enable-symmetry-breaker and --disable-symmetry-breaker
options that are always respected regardless of this default.

Expected performance impact: positive

New default (UF only) compared to old default (always on):
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5

Symmetry breaker remains a big win on UF:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5

The last link to results looks at first that the symmetry breaker should
always be turned off, since its use loses more regressions than it gains.
*However*, the lost ones are only our "QF_SAT" benchmarks.  For these, we
should indeed turn off the symmetry breaker, but that's impossible for
now because we tag them internally with the logic "QF_UF."

0 files changed, 0 insertions, 0 deletions