My previous commit changed the regular timeout of paramodulation from

infinity to 30s. Old behaviour restored.

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 305a42ab1adfab718e77d1e4d8f33bd7b919045e..194f05dc936a62396bd5f253423faf5da865a13d 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -555,10 +555,12 @@ let int params name default =
         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 ;;  
 
-let flags_of_params params ?(use_only_paramod = bool params "paramodulation" false) () =
+let flags_of_params params ?(for_applyS=false) () =
  let int = int params in
  let bool = bool params in
  let use_paramod = bool "use_paramod" true in
+ let use_only_paramod =
+  if for_applyS then true else bool "paramodulation" true in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let timeout = int "timeout" 0 in
@@ -567,7 +569,7 @@ let flags_of_params params ?(use_only_paramod = bool params "paramodulation" fal
     AutoTypes.maxwidth = width;
     AutoTypes.timeout = 
       if timeout = 0 then
-       if use_only_paramod then Unix.gettimeofday () +. 30.0
+       if for_applyS then Unix.gettimeofday () +. 30.0
        else
         0.0
       else
@@ -583,7 +585,7 @@ let applyS_tac ~dbd ~term ~params =
     try 
       let _, proof, gl,_,_ =
        apply_smart ~dbd ~term ~subst:[]
-        (flags_of_params params ~use_only_paramod:true ()) status
+        (flags_of_params params ~for_applyS:true ()) status
       in 
        proof, gl
     with