50 steps on goal are fine for irrat2

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 2db8cc0014ec1d468b60df2872caff898fba9c57..c65826a4feab8e9e319df6219c65a8db70d516ca 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,7 +26,7 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug_print s = () (* prerr_endline s;; *)
+let debug_print s = () (*prerr_endline s;;*)
 
 (* {{{ *********** local given_clause wrapper ***********)
 
@@ -59,7 +59,7 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
         let passive = Saturation.add_to_passive equalities passive in
         let goal_steps, saturation_steps, timeout =
           if flags.use_only_paramod then max_int,max_int,flags.timeout
-          else max 80 minsteps, minsteps, infinity
+          else max 50 minsteps, minsteps, infinity
         in
         active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
   in
@@ -274,9 +274,11 @@ let equational_case
 =
   let ppterm = ppterm context in
   prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
+(*
   prerr_endline "<CACHE>";
   prerr_endline (cache_print context cache);
   prerr_endline "</CACHE>";
+*)
   match 
     given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) 
   with
@@ -356,7 +358,8 @@ let is_equational_case goalty flags =
   (flags.use_only_paramod && ensure_equational goalty)
 ;;
 let cache_add_success sort cache k v =
-  if sort = P then cache_add_success cache k v else cache
+  if sort = P then cache_add_success cache k v else cache_remove_underinspection
+  cache k
 ;;
 
 let rec auto_main dbd tables maxm context flags elems cache =
@@ -476,7 +479,7 @@ let rec auto_main dbd tables maxm context flags elems cache =
                 depth fake_proof goalno goalty subst context flags 
             with
             | Some elems, tables, cache, maxm -> 
-                elems, tables, cache, maxm (* manca cache *)
+                elems, tables, cache, maxm 
             | None, tables,cache,maxm -> 
                 applicative_case dbd tables maxm depth subst fake_proof goalno 
                   goalty metasenv context cache