revert %T and use another technique

drivers/vampire.drv

@@ -4,8 +4,8 @@ printer "tptp"
 filename "%f-%t-%g.p"
 
 valid   "Refutation found"
-timeout "Aborted by signal SIGXCPU on"
-timeout "Time limit reached"
+(* timeout "Aborted by signal SIGXCPU on" *)
+unknown "Time limit reached" "Time out"
 unknown "Refutation not found" "Unknown"
 (* invalid "Completion found" *)
 (* invalid "SZS status CounterSatisfiable" *)

examples/einstein/why3session.xml

@@ -75,19 +75,12 @@
     proved="true"
     expanded="true"
     shape="ainfix =ato_aFishaGerman">
-    <proof
-     prover="alt-ergo"
-     timelimit="2"
-     edited=""
-     obsolete="false">
-     <result status="timeout" time="2.02"/>
-    </proof>
     <proof
      prover="cvc3"
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="valid" time="2.70"/>
+     <result status="valid" time="2.53"/>
     </proof>
     <proof
      prover="z3"
@@ -101,7 +94,7 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="2.99"/>
+     <result status="timeout" time="4.96"/>
     </proof>
     <proof
      prover="yices"
@@ -115,14 +108,14 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="3.98"/>
+     <result status="unknown" time="5.08"/>
     </proof>
     <proof
      prover="spass"
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="2.99"/>
+     <result status="timeout" time="4.99"/>
     </proof>
    </goal>
    <goal
@@ -131,19 +124,12 @@
     proved="false"
     expanded="true"
     shape="ainfix =ato_aCatsaSwede">
-    <proof
-     prover="alt-ergo"
-     timelimit="2"
-     edited=""
-     obsolete="false">
-     <result status="timeout" time="2.02"/>
-    </proof>
     <proof
      prover="cvc3"
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="3.02"/>
+     <result status="timeout" time="5.04"/>
     </proof>
     <proof
      prover="z3"
@@ -157,7 +143,7 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="2.98"/>
+     <result status="timeout" time="4.97"/>
     </proof>
     <proof
      prover="yices"
@@ -171,14 +157,14 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="3.98"/>
+     <result status="unknown" time="4.88"/>
     </proof>
     <proof
      prover="spass"
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="3.06"/>
+     <result status="timeout" time="4.69"/>
     </proof>
    </goal>
    <goal
@@ -187,19 +173,12 @@
     proved="true"
     expanded="true"
     shape="ainfix =ato_aCatsaNorwegian">
-    <proof
-     prover="alt-ergo"
-     timelimit="2"
-     edited=""
-     obsolete="false">
-     <result status="timeout" time="2.02"/>
-    </proof>
     <proof
      prover="cvc3"
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="valid" time="2.04"/>
+     <result status="valid" time="1.94"/>
     </proof>
     <proof
      prover="z3"
@@ -213,7 +192,7 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="2.99"/>
+     <result status="timeout" time="4.98"/>
     </proof>
     <proof
      prover="yices"
@@ -227,14 +206,14 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="3.98"/>
+     <result status="unknown" time="4.97"/>
     </proof>
     <proof
      prover="spass"
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="timeout" time="2.99"/>
+     <result status="timeout" time="4.77"/>
     </proof>
    </goal>
   </theory>

share/provers-detection-data.conf.in

@@ -38,7 +38,8 @@ version_switch = "-version"
 version_regexp = "This is CVC3 version \\([^ \n]+\\)"
 version_ok = "2.2"
 version_old = "2.1"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -timeout %T %f"
+# we pass time 0 to why3-cpulimit to avoid race
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t %f"
 driver = "drivers/cvc3.drv"
 
 [ATP yices]
@@ -61,10 +62,9 @@ name = "Eprover"
 exec = "eprover"
 version_switch = "--version"
 version_regexp = "E \\([^\n]+\\)"
-version_ok = "1.4 Namring"
-# we pass %T ie time+1 to e-prover, 
-# to avoid replacing answer "timeout" by "unknown"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -s -R -xAuto -tAuto --cpu-limit=%T --tstp-in %f"
+version_ok = "1.4 Namring"   
+# we pass time 0 to why3-cpulimit to avoid race
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
 driver = "drivers/tptp.drv"
 
 [ATP gappa]
@@ -104,9 +104,8 @@ exec = "SPASS"
 version_switch = "-TPTP || true"
 version_regexp = "SPASS V \\([^ \n\t]+\\)"
 version_ok = "3.7"
-# we pass %T ie time+1 to spass, 
-# to avoid replacing answer "timeout" by "unknown"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%T %f"
+# we pass time 0 to why3-cpulimit to avoid race
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
 driver = "drivers/tptp.drv"
 
 [ATP vampire]
@@ -114,9 +113,8 @@ name = "Vampire"
 exec = "vampire"
 version_switch = "--version"
 version_regexp = "Vampire \\([0-9.]+\\)"
-# we pass %T ie time+1 to vampire, 
-# to avoid replacing answer "timeout" by "unknown"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -t %T"
+# we pass time 0 to why3-cpulimit to avoid race
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -t %t"
 driver = "drivers/vampire.drv"
 version_ok = "0.6"
 

src/driver/call_provers.ml

@@ -128,7 +128,6 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
     | "%" -> "%"
     | "f" -> file
     | "t" -> on_timelimit := true; string_of_int timelimit
-    | "T" -> on_timelimit := true; string_of_int (timelimit+1)
     | "m" -> string_of_int memlimit
     | "b" -> string_of_int (memlimit * 1024)
     | _ -> failwith "unknown format specifier, use %%f, %%t, %%m or %%b"