Session: default steplimit -1 does not need to be stored

examples/linked_list_rev/why3session.xml

@@ -5,7 +5,7 @@
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="1" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="1" memlimit="1000"/>
-<prover id="6" name="Z3" version="4.4.0" timelimit="36" steplimit="-1" memlimit="1000"/>
+<prover id="6" name="Z3" version="4.4.0" timelimit="36" memlimit="1000"/>
 <file name="../linked_list_rev.mlw" expanded="true">
 <theory name="Disjoint" sum="d9538770c8f60c61e92f6baffbf62d5d">
  <goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
@@ -137,8 +137,8 @@
  <goal name="non_empty_seq">
  <proof prover="3"><result status="valid" time="0.02" steps="22"/></proof>
  </goal>
- <goal name="WP_parameter mem_decomp" expl="VC for mem_decomp" expanded="true">
- <transf name="split_goal_wp" expanded="true">
+ <goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
+ <transf name="split_goal_wp">
   <goal name="WP_parameter mem_decomp.1" expl="1. postcondition">
   <proof prover="3"><result status="valid" time="0.02" steps="27"/></proof>
   </goal>
@@ -151,7 +151,7 @@
   <goal name="WP_parameter mem_decomp.4" expl="4. precondition">
   <proof prover="6"><result status="valid" time="0.05"/></proof>
   </goal>
-  <goal name="WP_parameter mem_decomp.5" expl="5. postcondition" expanded="true">
+  <goal name="WP_parameter mem_decomp.5" expl="5. postcondition">
   <proof prover="3" timelimit="36" steplimit="-1"><result status="valid" time="0.12" steps="165"/></proof>
   </goal>
  </transf>

src/session/session.ml

@@ -795,13 +795,18 @@ let get_prover_to_save prover_ids p (timelimits,steplimits,memlimits) provers =
 
 
 let save_prover fmt id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) =
+  let steplimit =
+    if mostfrequent_steplimit < 0 then None else Some mostfrequent_steplimit
+  in
   fprintf fmt "@\n@[<h><prover@ id=\"%i\"@ name=\"%a\"@ \
-               version=\"%a\"%a@ timelimit=\"%d\"@ steplimit=\"%d\"@ memlimit=\"%d\"/>@]"
+               version=\"%a\"%a@ timelimit=\"%d\"%a@ memlimit=\"%d\"/>@]"
     id save_string p.C.prover_name save_string p.C.prover_version
     (fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
         save_string s)
     p.C.prover_altern
-    mostfrequent_timelimit mostfrequent_steplimit mostfrequent_memlimit
+    mostfrequent_timelimit
+    (opt pp_print_int "steplimit") steplimit
+    mostfrequent_memlimit
 
 let save fname shfname _config session =
   let ch = open_out fname in