Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-29 18:44:04 -0800 (Mon, 29 Nov 2004)
Revision: 6293
Log message:

      1. Fixed two bugs in old code (since spring)
      2. Now it's more like Shostak's version - if first variable did not produce
      a contradiction it attempts the next variable, etc.
      ToDo: If SupInf computed that a<=v<=b and there is no integer between
      a and b we can conclude a contradiction.
      

Changes	Path
+58 -13	metaprl/refiner/reflib/supinf.ml
+4 -1	metaprl/refiner/reflib/supinf.mli
+154 -103	metaprl/theories/itt/itt_supinf.ml