Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-28 11:55:53 -0800 (Tue, 28 Dec 2004)
Revision: 6362
Log message:

      gen_int_bench generates two benchmarks itt_int_bench and itt_int_bench2
      for arithmetical tactics.
      On those tests SupInf consumes more than 400Mb and I have to terminate it
      (I will investigate if memory consumption can be optimized)
      Omega Test proves about 50% of tests (5 out of 10, they are not guaranteed to be provable)
      in 50 and 40 seconds respectfully consuming about 100Mb.
      Unfortunately on the other 50% of tests Omega crashes MetaPRL (under Cygwin) -
      will investigate.
      

Changes	Path
+1 -1	metaprl/OMakefile
Properties	metaprl/theories/itt
+14 -0	metaprl/theories/itt/OMakefile
Added	metaprl/theories/itt/gen_int_bench.ml
Properties	metaprl/theories/itt/gen_int_bench.ml
Added	metaprl/theories/itt/itt_int_bench.prla
Properties	metaprl/theories/itt/itt_int_bench.prla
Added	metaprl/theories/itt/itt_int_bench2.prla
Properties	metaprl/theories/itt/itt_int_bench2.prla