Drivers : In a driver, the regexps are

tested in the same order as they appear in the file.

src/driver/call_provers.mli

@@ -52,7 +52,11 @@ val print_prover_result : Format.formatter -> prover_result -> unit
     a [HighFailure] *)
 
 val debug : Debug.flag
-(** debug flag for the calling procedure (option "--debug call_prover") *)
+(** debug flag for the calling procedure (option "--debug
+    call_prover")
+    If set [call_on_buffer] prints on stderr the commandline called
+    and the output of the prover.
+*)
 
 val call_on_buffer :
   command    : string ->
@@ -63,6 +67,20 @@ val call_on_buffer :
   filename   : string ->
   Buffer.t -> unit -> prover_result
 (** Call a prover on the task printed in the {!type: Buffer.t} given.
-    @param debug : set the debug flag.
-    Print on stderr the commandline called and the output of the prover. *)
+
+    @param timelimit : set the available time limit (default 0 : unlimited)
+    @param memlimit : set the available time limit (default 0 :
+    unlimited)
+
+    @param regexps : if the first field match the prover output the
+    second field is the answer. Regexp groups present in the first field are
+    substituted in the second field (\0,\1,...). The regexp are tested in the
+    order of the list.
+    @param exitcodes : if the first field is the exit code the second
+    field is the answer. No subtitution are done. Exit codes are tested
+    in the order of the list and before the regexps.
+
+    @param filename : if the prover doesn't accept stdin, a temporary
+    file is used. In the case the suffix of the temporary file is
+    [filename] *)
 

src/driver/driver.ml

@@ -167,8 +167,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
     drv_thprelude = !thprelude;
     drv_meta      = !meta;
     drv_meta_cl   = !meta_cl;
-    drv_regexps   = !regexps;
-    drv_exitcodes = !exitcodes;
+    drv_regexps   = List.rev !regexps;
+    drv_exitcodes = List.rev !exitcodes;
   }
 
 (** apply drivers *)