Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-02-20 00:56:01 -0800 (Sun, 20 Feb 2005)
Revision: 6725
Log message:

      More improvements for constraint that unfolds to
      D1 \/ D2
      if when solving D1-case D1 was not actually used we now skip D2
      altogether.
      It reduced total time on my "long" benchmark from 260 to 130 seconds.
      Time on omega itself is approximately 70 seconds.
      

Changes  Path
+55 -9 metaprl/theories/itt/itt_omega.ml