Merge branch 'counter-examples'

doc/manpages.tex

@@ -450,6 +450,20 @@ are grouped together under several tabs.
   decision by clicking on it.
 \end{description}
 
+% \subsection{Displaying Counterexamples}
+%
+% how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
+%
+% problem with set logic and counterexamples
+%
+% which provers
+%
+% where it is displayed
+%
+% how to interpret the display
+%
+% example
+
 \subsection{Additional Command-Line Options}
 
 The \texttt{ide} command also accepts the following options described for the command \texttt{prove} in Section~\ref{sec:proveoptions}.

drivers/cvc4_15.drv

@@ -12,9 +12,6 @@ prelude "(set-logic AUFBVDTLIRA)"
    does not seem to include DT
 *)
 
-(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
-(* transformation "split_intro" *)
-
 (* Counterexamples: set model parser *)
 model_parser "smtv2"
 
@@ -24,9 +21,7 @@ import "discrimination.gen"
 
 transformation "inline_trivial"
 transformation "eliminate_builtin"
-(* temporarily disabled: too much experimental
 transformation "detect_polymorphism"
-*)
 transformation "eliminate_definition_if_poly"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic_if_poly"

examples/tests/cvc4-models.mlw

@@ -22,7 +22,11 @@ module M
   ensures { !x < old !x }
   =
   incr x;
-  while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
+  while "model" "model_trace:cond" !x > 0 do
+  invariant { !x >= 0 }
+  variant { !x }
+    x := !x - 1
+  done
 
   (**************************************
    ** Getting counterexamples for maps **

examples/use_api/create_session.ml

@@ -93,6 +93,7 @@ let add_proofs_attempts g =
           ~obsolete:true
           ~archived:false
           ~timelimit:5
+	  ~steplimit:(-1)
           ~memlimit:1000
           ~edit:None
           g p.Whyconf.prover Session.Scheduled
@@ -106,5 +107,3 @@ let () =
 
 (* save the session on disk *)
 let () = Session.save_session config env_session.Session.session
-
-

src/coq-tactic/why3tac.ml4

@@ -1285,7 +1285,7 @@ let why3tac ?(timelimit=timelimit) s gl =
     match res.pr_answer with
       | Valid -> admit_as_an_axiom gl
       | Invalid -> error "Invalid"
-      | Unknown s -> error ("Don't know: " ^ s)
+      | Call_provers.Unknown (s, _) -> error ("Don't know: " ^ s)
       | Call_provers.Failure s -> error ("Failure: " ^ s)
       | Call_provers.Timeout -> error "Timeout"
       | OutOfMemory -> error "Out Of Memory"

src/driver/call_provers.ml

@@ -16,6 +16,29 @@ let debug = Debug.register_info_flag "call_prover"
   ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
          and@ keep@ temporary@ files."
 
+type reason_unknown =
+  | Resourceout
+  | Other
+
+type prover_answer =
+  | Valid
+  | Invalid
+  | Timeout
+  | OutOfMemory
+  | StepLimitExceeded
+  | Unknown of (string * reason_unknown option)
+  | Failure of string
+  | HighFailure
+
+type prover_result = {
+  pr_answer : prover_answer;
+  pr_status : Unix.process_status;
+  pr_output : string;
+  pr_time   : float;
+  pr_steps  : int;		(* -1 if unknown *)
+  pr_model  : model;
+}
+
 (** time regexp "%h:%m:%s" *)
 type timeunit =
   | Hour
@@ -83,26 +106,15 @@ let rec grep_steps out = function
       with _ -> grep_steps out l
     end
 
-(** *)
-
-type prover_answer =
-  | Valid
-  | Invalid
-  | Timeout
-  | OutOfMemory
-  | StepLimitExceeded
-  | Unknown of string
-  | Failure of string
-  | HighFailure
-
-type prover_result = {
-  pr_answer : prover_answer;
-  pr_status : Unix.process_status;
-  pr_output : string;
-  pr_time   : float;
-  pr_steps  : int;		(* -1 if unknown *)
-  pr_model  : model;
-}
+let grep_reason_unknown out =
+  try
+    let re = Str.regexp "^(:reason-unknown \\([^)]*\\)" in
+    ignore (Str.search_forward re out 0);
+    match  (Str.matched_group 1 out) with
+    | "resourceout" -> Resourceout
+    | _ -> Other
+  with Not_found ->
+    Other
 
 type prover_result_parser = {
   prp_regexps     : (Str.regexp * prover_answer) list;
@@ -112,15 +124,20 @@ type prover_result_parser = {
   prp_model_parser : Model_parser.model_parser;
 }
 
+let print_unknown_reason fmt r =
+  match r with
+  | Some Resourceout -> fprintf fmt " because of resource limit reached "
+  | _ -> ()
+
 let print_prover_answer fmt = function
   | Valid -> fprintf fmt "Valid"
   | Invalid -> fprintf fmt "Invalid"
   | Timeout -> fprintf fmt "Timeout"
   | OutOfMemory -> fprintf fmt "Ouf Of Memory"
   | StepLimitExceeded -> fprintf fmt "Step limit exceeded"
-  | Unknown "" -> fprintf fmt "Unknown"
+  | Unknown ("", r) -> fprintf fmt "Unknown%a" print_unknown_reason r
   | Failure "" -> fprintf fmt "Failure"
-  | Unknown s -> fprintf fmt "Unknown (%s)" s
+  | Unknown (s, r) -> fprintf fmt "Unknown %a(%s)" print_unknown_reason r s
   | Failure s -> fprintf fmt "Failure (%s)" s
   | HighFailure -> fprintf fmt "HighFailure"
 
@@ -151,7 +168,7 @@ let rec grep out l = match l with
         ignore (Str.search_forward re out 0);
         match pa with
         | Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded -> pa
-        | Unknown s -> Unknown (Str.replace_matched s out)
+        | Unknown (s, ru) -> Unknown ((Str.replace_matched s out), ru)
         | Failure s -> Failure (Str.replace_matched s out)
         | HighFailure -> assert false
       with Not_found -> grep out l end
@@ -188,6 +205,10 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
   Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
   let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
   let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepregexps) in
+  let reason_unknown = grep_reason_unknown out in
+  let ans = match ans with
+    | Unknown (s, _) -> Unknown (s, Some reason_unknown)
+    | _ -> ans in
   let ans = match ans with
     | Unknown _ | HighFailure when on_timelimit && timelimit > 0
       && time >= (0.9 *. float timelimit) -> Timeout

src/driver/call_provers.mli

@@ -15,6 +15,13 @@ open Model_parser
 
 (** {2 data types for prover answers} *)
 
+(** The reason why unknown was reported *)
+type reason_unknown =
+  | Resourceout
+  (** Out of resources  *)
+  | Other
+  (** Other reason *)
+
 type prover_answer =
   | Valid
       (** The task is valid according to the prover *)
@@ -26,7 +33,7 @@ type prover_answer =
       (** the task runs out of memory *)
   | StepLimitExceeded
       (** the task required more steps than the limit provided *)
-  | Unknown of string
+  | Unknown of (string * reason_unknown option)
       (** The prover can't determine if the task is valid *)
   | Failure of string
       (** The prover reports a failure *)
@@ -45,8 +52,8 @@ type prover_result = {
   (** The time taken by the prover *)
   pr_steps  : int;
   (** The number of steps taken by the prover (-1 if not available) *)
-  (** The model produced by a the solver *)
   pr_model  : model;
+  (** The model produced by a the solver *)
 }
 
 val print_prover_answer : Format.formatter -> prover_answer -> unit

src/driver/driver.ml

@@ -92,7 +92,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | RegexpOutOfMemory s -> add_to_list regexps (Str.regexp s, OutOfMemory)
     | RegexpStepLimitExceeded s ->
       add_to_list regexps (Str.regexp s, StepLimitExceeded)
-    | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
+    | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown (t, None))
     | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
     | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
     | StepRegexp (r,ns) ->
@@ -103,7 +103,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | ExitCodeOutOfMemory s -> add_to_list exitcodes (s, OutOfMemory)
     | ExitCodeStepLimitExceeded s ->
       add_to_list exitcodes (s, StepLimitExceeded)
-    | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
+    | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown (t, None))
     | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
     | Filename s -> set_or_raise loc filename s "filename"
     | Printer s -> set_or_raise loc printer s "printer"

src/driver/parse_smtv2_model_lexer.mll

@@ -13,6 +13,7 @@ rule token = parse
     { token lexbuf }
   | space+ as space_str
       { SPACE (space_str) }
+  | "mk_t__ref"(num*) { MK_T_REF }
   | "store" { STORE }
   | "const" { CONST }
   | "as" { AS }

src/driver/parse_smtv2_model_parser.mly

@@ -13,6 +13,7 @@
 %token <string * string> DEC_STR
 %token <string * string> MINUS_DEC_STR
 %token LPAREN RPAREN
+%token MK_T_REF
 %token EOF
 %%
 
@@ -53,6 +54,7 @@ text_without_int:
 | AS { "as" }
 
 value:
+| LPAREN MK_T_REF SPACE value RPAREN { $4 }
 | integer { $1 }
 | decimal { $1 }
 | other_val_str { Model_parser.Unparsed $1 }

src/ide/gmain.ml

@@ -1016,7 +1016,7 @@ let prover_on_selected_goals pr =
        M.run_prover
          (env_session()) sched
          ~context_unproved_goals_only:!context_unproved_goals_only
-         ~cntexample ~timelimit ~memlimit
+         ~cntexample ~timelimit ~steplimit:(-1) ~memlimit
          pr a
       with e ->
         eprintf "@[Exception raised while running a prover:@ %a@.@]"
@@ -1541,11 +1541,11 @@ let test_strategy () =
     Whyconf.filter_one_prover config fp
   in
   [|
-    Strategy.Icall_prover(altergo.Whyconf.prover,1,1000);
-    Strategy.Icall_prover(cvc4.Whyconf.prover,1,1000);
+    Strategy.Icall_prover(altergo.Whyconf.prover,1,-1,1000);
+    Strategy.Icall_prover(cvc4.Whyconf.prover,1,0,1000);
     Strategy.Itransform(split_transformation,0); (* goto 0 on success *)
-    Strategy.Icall_prover(altergo.Whyconf.prover,10,4000);
-    Strategy.Icall_prover(cvc4.Whyconf.prover,10,4000);
+    Strategy.Icall_prover(altergo.Whyconf.prover,10,-1,4000);
+    Strategy.Icall_prover(cvc4.Whyconf.prover,10,-1,4000);
   |]
 
 (*

src/printer/smtv2.ml

@@ -176,11 +176,33 @@ let model_label = Ident.create_label "model"
 let model_vc_term_label = Ident.create_label "model_vc"
   (* This label identifies the term that triggers the VC. *)
 
+let add_model_element el info_model =
+(** Add element el (term) to info_model.
+    If an element with the same hash (the same set of labels + the same
+    location) as the element el already exists in info_model, replace it with el.
+
+    The reason is that  we do not want to display two model elements with the same
+    name in the same location and usually it is better to display the last one.
+
+    Note that two model elements can have the same name and location if why is used
+    as an intemediate language and the locations are locations in the source language.
+    Then, more why constructs (terms) can represent a single construct in the source
+    language and more terms have thus the same model name and location. This happens,
+    e.g., if why code is generated from SPARK. There, the first iteration of while
+    cycle is unrolled in some cases. If the task contains both a term representing a
+    variable in the first iteration of unrolled loop and a term representing the variable
+    in the subsequent loop iterations, only the latter is relevant for the counterexample
+    and it is the one that comes after the former one (and that is why we always keep the
+    last term).
+*)
+  let info_model = S.remove el info_model in
+  S.add el info_model
+
 let collect_model_ls info ls =
   if ls.ls_args = [] && Slab.mem model_label ls.ls_name.id_label then
     let t = t_app ls [] ls.ls_value in
     info.info_model <-
-      S.add
+      add_model_element
       (t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) info.info_model
 
 let model_trace_regexp = Str.regexp "model_trace:"
@@ -267,7 +289,7 @@ let rec print_term info fmt t =
   debug_print_term "Printing term: " t;
 
   if Slab.mem model_label t.t_label then
-    info.info_model <- S.add t info.info_model;
+    info.info_model <- add_model_element t info.info_model;
 
   check_enter_vc_term t info;
 
@@ -318,7 +340,7 @@ let rec print_term info fmt t =
 		    model_trace_for_postcondition ~labels:ls.ls_name.id_label info in
 		let _t_check_pos = t_label ~loc labels t in
 		(* TODO: temporarily disable collecting variables inside the term triggering VC *)
-		(*info.info_model <- S.add t_check_pos info.info_model;*)
+		(*info.info_model <- add_model_element t_check_pos info.info_model;*)
 		()
 	    end;
 	    fprintf fmt "@[%a@]" print_ident ls.ls_name
@@ -361,7 +383,7 @@ let rec print_term info fmt t =
 and print_fmla info fmt f =
   debug_print_term "Printing formula: " f;
   if Slab.mem model_label f.t_label then
-    info.info_model <- S.add f info.info_model;
+    info.info_model <- add_model_element f info.info_model;
 
   check_enter_vc_term f info;
 
@@ -560,6 +582,8 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
       let model_list = S.elements info.info_model in
       fprintf fmt "@[(check-sat)@]@\n";
       print_info_model cntexample fmt model_list info;
+      (* (get-info :reason-unknown) *)
+      fprintf fmt "@[(get-info :reason-unknown)@]@\n";
 
       args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
 				vc_term_loc = vc_loc;

src/session/session.mli

@@ -96,6 +96,7 @@ and 'a proof_attempt = private
       proof_parent : 'a goal;
       mutable proof_state : proof_attempt_status;
       mutable proof_timelimit : int;
+      mutable proof_steplimit : int;
       mutable proof_memlimit : int;
       mutable proof_obsolete : bool;
       mutable proof_archived : bool;
@@ -346,6 +347,7 @@ val add_external_proof :
   obsolete:bool ->
   archived:bool ->
   timelimit:int ->
+  steplimit:int ->
   memlimit:int ->
   edit:string option ->
   'key goal ->
@@ -388,6 +390,7 @@ val copy_external_proof :
   ?obsolete:bool ->
   ?archived:bool ->
   ?timelimit:int ->
+  ?steplimit:int ->
   ?memlimit:int ->
   ?edit:string option ->
   ?goal:'key goal ->

src/session/session_scheduler.ml

@@ -290,7 +290,7 @@ let schedule_proof_attempt ~cntexample ~timelimit ~memlimit ~steplimit ?old ~inp
 let schedule_edition t command filename callback =
   Debug.dprintf debug "[Sched] Scheduling an edition@.";
   let res_parser =
-    { Call_provers.prp_exitcodes = [(0,Call_provers.Unknown "")];
+    { Call_provers.prp_exitcodes = [(0,Call_provers.Unknown ("", None))];
       Call_provers.prp_regexps = [];
       Call_provers.prp_timeregexps = [];
       Call_provers.prp_stepregexps = [];
@@ -545,7 +545,7 @@ let run_external_proof eS eT ?(cntexample=false) ?callback a =
   in
   run_external_proof_v2 ~use_steps:false eS eT a ~cntexample callback
 
-let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g =
+let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~steplimit ~memlimit p g =
   let a =
     try
       let a = PHprover.find g.goal_external_proofs p in
@@ -554,7 +554,7 @@ let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g
       a
     with Not_found ->
       let ep = add_external_proof ~keygen:O.create ~obsolete:false
-        ~archived:false ~timelimit ~memlimit
+        ~archived:false ~timelimit ~steplimit ~memlimit
         ~edit:None g p Interrupted in
       O.init ep.proof_key (Proof_attempt ep);
       ep
@@ -562,39 +562,39 @@ let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g
   run_external_proof eS eT ~cntexample ?callback a
 
 let prover_on_goal_or_children eS eT
-    ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit p g =
+    ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit p g =
   goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
-    (prover_on_goal eS eT ~cntexample ~timelimit ~memlimit p) g
+    (prover_on_goal eS eT ~cntexample ~timelimit ~steplimit ~memlimit p) g
 
-let run_prover eS eT ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr a =
+let run_prover eS eT ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr a =
   match a with
   | Goal g ->
     prover_on_goal_or_children eS eT
-      ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr g
+      ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr g
   | Theory th ->
         List.iter
           (prover_on_goal_or_children eS eT
-             ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
+             ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr)
           th.theory_goals
     | File file ->
         List.iter
           (fun th ->
              List.iter
                (prover_on_goal_or_children eS eT
-                  ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
+                  ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr)
                th.theory_goals)
           file.file_theories
     | Proof_attempt a ->
         prover_on_goal_or_children eS eT
-          ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr a.proof_parent
+          ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr a.proof_parent
     | Transf tr ->
         List.iter
           (prover_on_goal_or_children eS eT
-             ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
+             ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr)
           tr.transf_goals
     | Metas m ->
       prover_on_goal_or_children eS eT
-        ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr m.metas_goal
+        ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr m.metas_goal
 
 
 
@@ -741,16 +741,17 @@ let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
 (* play all                        *)
 (***********************************)
 
-let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
-  let timelimit, memlimit, auto_proved =
-    PHprover.fold (fun _ pa (timelimit, memlimit, _ as acc) ->
+let rec play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l g =
+  let timelimit, steplimit, memlimit, auto_proved =
+    PHprover.fold (fun _ pa (timelimit, steplimit, memlimit, _ as acc) ->
       match pa.proof_edited_as, pa.proof_state with
         | None, Done { Call_provers.pr_answer = Call_provers.Valid } ->
             max timelimit pa.proof_timelimit,
+	    max steplimit pa.proof_steplimit,
             max memlimit pa.proof_memlimit,
             true
         | _ -> acc)
-      g.goal_external_proofs (timelimit, memlimit, false) in
+      g.goal_external_proofs (timelimit, steplimit, memlimit, false) in
   let callback _key status =
     if not (running status) then Todo._done todo () in
   if auto_proved then begin
@@ -760,21 +761,21 @@ let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
       (* eprintf "todo increased to %d@." todo.Todo.todo; *)
       (* eprintf "prover %a on goal %s@." *)
       (*   Whyconf.print_prover p g.goal_name.Ident.id_string; *)
-        prover_on_goal eS eT ~callback ~timelimit ~memlimit p g)
+        prover_on_goal eS eT ~callback ~timelimit ~steplimit ~memlimit p g)
       l
   end;
   iter_goal
     (fun _ -> ())
     (iter_transf
-       (play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
+       (play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l)
     )
     (iter_metas
-       (play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
+       (play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l)
     )
     g
 
 
-let play_all eS eT ~callback ~timelimit ~memlimit l =
+let play_all eS eT ~callback ~timelimit ~steplimit ~memlimit l =
   let todo = Todo.create () (fun () _ -> ()) callback in
   Todo.start todo;
   PHstr.iter
@@ -782,7 +783,7 @@ let play_all eS eT ~callback ~timelimit ~memlimit l =
       List.iter
         (fun th ->
           List.iter
-            (play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
+            (play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l)
             th.theory_goals)
         file.file_theories)
     eS.session.session_files;
@@ -861,7 +862,7 @@ let edit_proof ~cntexample eS sched ~default_editor a =
   else
     let callback a res =
       match res with
-      | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
+      | Done {Call_provers.pr_answer = Call_provers.Unknown ("", None)} ->
         set_proof_state ~notify ~obsolete:true ~archived:false
           JustEdited a
       | _ ->
@@ -873,7 +874,7 @@ let edit_proof ~cntexample eS sched ~default_editor a =
 let edit_proof_v3 ~cntexample eS sched ~default_editor ~callback a =
   let callback a res =
     match res with
-    | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
+    | Done {Call_provers.pr_answer = Call_provers.Unknown ("", None)} ->
       callback a
     | _ -> ()
   in
@@ -939,7 +940,7 @@ let convert_unknown_prover =
       Todo._done todo ()
     else
       match Array.get strat pc with
-        | Icall_prover(p,timelimit,memlimit) ->
+        | Icall_prover(p,timelimit,steplimit,memlimit) ->
           let callback _pa res =
             match res with
               | Scheduled | Running ->
@@ -956,7 +957,7 @@ let convert_unknown_prover =
                 (* should not happen *)
                 assert false
           in
-          prover_on_goal es sched ~callback ~timelimit ~memlimit p g
+          prover_on_goal es sched ~callback ~timelimit ~steplimit ~memlimit p g
         | Itransform(trname,pcsuccess) ->
           let callback ntr =
             match ntr with

src/session/session_scheduler.mli

@@ -133,7 +133,7 @@ module Make(O: OBSERVER) : sig
     O.key env_session -> t ->
     context_unproved_goals_only:bool ->
     cntexample : bool ->
-    timelimit:int -> memlimit:int ->
+    timelimit:int -> steplimit:int -> memlimit:int ->
     Whyconf.prover -> O.key any -> unit
     (** [run_prover es sched p a] runs prover [p] on all goals under [a]
         the proof attempts are only scheduled for running, and they
@@ -188,7 +188,7 @@ module Make(O: OBSERVER) : sig
     O.key env_session -> t ->
     ?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
     ?cntexample : bool ->
-    timelimit:int -> memlimit:int ->
+    timelimit:int -> steplimit:int -> memlimit:int ->
     Whyconf.prover -> O.key goal -> unit
   (** [prover_on_goal es sched ?cntexample ?timelimit p g] same as
       {!redo_external_proof} but creates or reuses existing proof_attempt
@@ -298,7 +298,7 @@ module Make(O: OBSERVER) : sig
 
   val play_all :
     O.key env_session -> t -> callback:(unit-> unit) ->
-    timelimit:int -> memlimit:int -> Whyconf.prover list -> unit
+    timelimit:int -> steplimit:int -> memlimit:int -> Whyconf.prover list -> unit
     (** [play_all es sched l] runs every prover of list [l] on all
         goals and sub-goals of the session, with the given time limit.
         [callback] is called when all tasks are finished.

src/session/strategy.ml

@@ -12,7 +12,7 @@
 (** {2 User-defined strategies} *)
 
 type instruction =
-  | Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
+  | Icall_prover of Whyconf.prover * int * int * int (** timelimit, steplimi, memlimit *)
   | Itransform of string * int (** successor state on success *)
   | Igoto of int (** goto state *)
 

src/session/strategy.mli

@@ -27,10 +27,8 @@
   *)
 
 type instruction =
-  | Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
+  | Icall_prover of Whyconf.prover * int * int * int (** timelimit, steplimi, memlimit *)
   | Itransform of string * int (** successor state on success *)
   | Igoto of int (** goto state *)
 
 type t = instruction array
-
-

src/session/strategy_parser.mll

@@ -120,13 +120,15 @@ rule scan code = parse
   | goto space+ (ident as id)
       { add_instr code (Igoto (find_label code id));
         scan code lexbuf }
-  | call space+ (ident as p) space+ (integer as t) space+ (integer as m)
+  | call space+ (ident as p) space+ (integer as t) space+ (integer as s) space+ (integer as m)
       { let p = prover code p in
         let t = integer "timelimit" t in
         if t <= 0 then error "timelimit %d is invalid" t;
+	let s = integer "steplimit" s in
+        if s <= 0 then error "steplimit %d is invalid" s;
         let m = integer "memlimit" m in
         if m <= 0 then error "memlimit %d is invalid" m;
-        add_instr code (Icall_prover (p.Whyconf.prover, t, m));
+        add_instr code (Icall_prover (p.Whyconf.prover, t, s, m));
         scan code lexbuf }
   | transform space+ (ident as t) space+ (ident as l)
       { transform code t;

src/tools/why3replay.ml

@@ -397,7 +397,7 @@ let run_as_bench env_session =
     eprintf " done.@.";
     exit 0
   in
-  M.play_all env_session sched ~callback ~timelimit:2 ~memlimit:0 provers;
+  M.play_all env_session sched ~callback ~timelimit:2 ~steplimit:(-1) ~memlimit:0 provers;
   main_loop ();
   eprintf "main replayer (in bench mode) exited unexpectedly@.";
   exit 1

src/transform/intro_vc_vars_counterexmp.ml

@@ -84,8 +84,7 @@ let model_trace_for_postcondition ~labels =
   (* Modifies the  model_trace label of a term in the postcondition:
      - if term corresponds to the initial value of a function
      parameter, model_trace label will have postfix @old
-     - if term corresponds to the return value of a function, add
-     model_trace label in a form function_name@result
+