Quoting :doc note-6-5:

  [Linear] arithmetic has been strengthened slightly so that
  immediately after simplification has ``settled down'' (see
  [hints-and-the-waterfall]), the unrewritten conclusion of a
  :[linear] rule may be used when normally this would not be the
  case. Thanks to Robert Krug for reminding us of examples we had
  encountered that could benefit from some such a change, and for
  pointing us to some relevant source code. This improvement
  generally causes an extra pass through the simplifier; hence we
  have observed approximately a 2% slowdown in the regression suite.
  Note that machinery is now in place for installing additional
  ``desperation heuristics''; perhaps the ACL2 community will have
  some to suggest.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1315 5d84a466-a78b-0930-a311-59b22171a541