Driver Alt-Ergo: uap directly Euclidean div and mod to Alt-Ergo

drivers/alt_ergo.drv

@@ -7,39 +7,6 @@ import "no-bv.gen"
 valid "^Inconsistent assumption$"
 
 
-theory int.EuclideanDivision
-
-  (* protection against wrong semantics for negative arguments
-    last checked on 1.20.prv: this is still needed
-  *)
-
-  prelude "logic safe_eucl_div: int, int -> int"
-  prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
-
-  prelude "logic safe_eucl_mod: int, int -> int"
-  prelude "axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y"
-
-  syntax function div "safe_eucl_div(%1,%2)"
-  syntax function mod "safe_eucl_mod(%1,%2)"
-
-end
-
-theory int.ComputerDivision
-
-  (* protection against wrong semantics for negative arguments
-    last checked on 1.20.prv: this is still needed
-  *)
-
-  prelude "logic safe_comp_div: int, int -> int"
-  prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
-
-  prelude "logic safe_comp_mod: int, int -> int"
-  prelude "axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y"
-
-  syntax function div "safe_comp_div(%1,%2)"
-  syntax function mod "safe_comp_mod(%1,%2)"
-
-end
 
 
 (*

drivers/alt_ergo_common.drv

@@ -88,6 +88,26 @@ theory int.Int
 
 end
 
+theory int.EuclideanDivision
+
+  syntax function div "(%1 / %2)"
+  syntax function mod "(%1 % %2)"
+
+end
+
+theory int.ComputerDivision
+
+  prelude "logic comp_div: int, int -> int"
+  prelude "axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y"
+
+  prelude "logic comp_mod: int, int -> int"
+  prelude "axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y"
+
+  syntax function div "comp_div(%1,%2)"
+  syntax function mod "comp_mod(%1,%2)"
+
+end
+
 
 theory real.Real
 

examples/WP_revisited/blocking_semantics5/why3session.xml

@@ -38,7 +38,7 @@
  <proof prover="0" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="0.80"/></proof>
  </goal>
 </theory>
-<theory name="TestSemantics" sum="5386d426772b7907db51e574cfc3e48a">
+<theory name="TestSemantics" sum="d19bd426b13b2949609e8ccb0829f621">
  <goal name="Test13">
  <proof prover="9"><result status="valid" time="0.02" steps="16"/></proof>
  <proof prover="10"><result status="valid" time="0.03"/></proof>
@@ -57,7 +57,7 @@
  <proof prover="9"><result status="valid" time="0.05" steps="107"/></proof>
  </goal>
  <goal name="If42">
- <proof prover="0" timelimit="6" edited="blocking_semantics5_TestSemantics_If42_1.v"><result status="valid" time="1.28"/></proof>
+ <proof prover="0" timelimit="6" edited="blocking_semantics5_TestSemantics_If42_1.v"><result status="valid" time="1.58"/></proof>
  </goal>
 </theory>
 <theory name="Typing" sum="d41d8cd98f00b204e9800998ecf8427e">
@@ -90,14 +90,14 @@
    <proof prover="9"><result status="valid" time="0.08" steps="143"/></proof>
    </goal>
    <goal name="eval_type_term.1.4" expl="4.">
-   <proof prover="0" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="1.57"/></proof>
+   <proof prover="0" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="2.24"/></proof>
    </goal>
   </transf>
   </goal>
  </transf>
  </goal>
  <goal name="type_preservation">
- <proof prover="0" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"><result status="valid" time="1.87"/></proof>
+ <proof prover="0" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"><result status="valid" time="2.30"/></proof>
  </goal>
 </theory>
 <theory name="FreshVariables" sum="490368b5a16b190f6c29edfc9b0d5a6b">
@@ -164,14 +164,14 @@
    <proof prover="9"><result status="valid" time="0.03" steps="79"/></proof>
    </goal>
    <goal name="eval_msubst.1.9" expl="9.">
-   <proof prover="3"><result status="valid" time="3.56"/></proof>
+   <proof prover="3"><result status="valid" time="4.08"/></proof>
    <proof prover="9" timelimit="30"><result status="valid" time="0.23" steps="586"/></proof>
    </goal>
    <goal name="eval_msubst.1.10" expl="10.">
    <proof prover="9"><result status="valid" time="0.30" steps="655"/></proof>
    </goal>
    <goal name="eval_msubst.1.11" expl="11.">
-   <proof prover="0" edited="blocking_semantics5_FreshVariables_eval_msubst_2.v"><result status="valid" time="1.21"/></proof>
+   <proof prover="0" edited="blocking_semantics5_FreshVariables_eval_msubst_2.v"><result status="valid" time="1.54"/></proof>
    </goal>
    <goal name="eval_msubst.1.12" expl="12.">
    <proof prover="9"><result status="valid" time="0.30" steps="561"/></proof>
@@ -189,7 +189,7 @@
    <proof prover="9"><result status="valid" time="0.04" steps="12"/></proof>
    </goal>
    <goal name="eval_swap_term.1.2" expl="2.">
-   <proof prover="0" edited="blocking_semantics5_FreshVariables_eval_swap_term_1.v"><result status="valid" time="1.36"/></proof>
+   <proof prover="0" edited="blocking_semantics5_FreshVariables_eval_swap_term_1.v"><result status="valid" time="1.68"/></proof>
    </goal>
    <goal name="eval_swap_term.1.3" expl="3.">
    <proof prover="3"><result status="valid" time="0.05"/></proof>
@@ -345,7 +345,7 @@
  <proof prover="3"><result status="valid" time="0.24"/></proof>
  </goal>
  <goal name="skip_rule">
- <proof prover="0" edited="blocking_semantics5_HoareLogic_skip_rule_1.v"><result status="valid" time="1.14"/></proof>
+ <proof prover="0" edited="blocking_semantics5_HoareLogic_skip_rule_1.v"><result status="valid" time="0.92"/></proof>
  </goal>
  <goal name="assign_rule">
  <proof prover="0" timelimit="12" edited="blocking_semantics5_HoareLogic_assign_rule_1.v"><result status="valid" time="1.86"/></proof>
@@ -379,7 +379,7 @@
    <proof prover="12"><result status="valid" time="0.10"/></proof>
    </goal>
    <goal name="monotonicity.1.2" expl="2.">
-   <proof prover="0" timelimit="30" edited="blocking_semantics5_WP_monotonicity_1.v"><result status="valid" time="1.45"/></proof>
+   <proof prover="0" timelimit="30" edited="blocking_semantics5_WP_monotonicity_1.v"><result status="valid" time="1.70"/></proof>
    </goal>
    <goal name="monotonicity.1.3" expl="3.">
    <proof prover="3" timelimit="5"><result status="valid" time="0.14"/></proof>
@@ -428,7 +428,7 @@
  </transf>
  </goal>
  <goal name="wp_preserved_by_reduction">
- <proof prover="0" memlimit="4000" edited="blocking_semantics5_WP_wp_preserved_by_reduction_4.v"><result status="valid" time="2.24"/></proof>
+ <proof prover="0" memlimit="4000" edited="blocking_semantics5_WP_wp_preserved_by_reduction_4.v"><result status="valid" time="2.84"/></proof>
  </goal>
  <goal name="progress">
  <transf name="induction_ty_lex">

examples/bitwalker/why3session.xml

@@ -9,6 +9,8 @@
 <prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="7" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="8" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../bitwalker.mlw" expanded="true">
 <theory name="Bitwalker" sum="6755724df7c462879051ab2676cc5753" expanded="true">
  <goal name="nth64">
@@ -162,8 +164,8 @@
   </goal>
  </transf>
  </goal>
- <goal name="WP_parameter peek" expl="VC for peek" expanded="true">
- <transf name="split_goal_wp" expanded="true">
+ <goal name="WP_parameter peek" expl="VC for peek">
+ <transf name="split_goal_wp">
   <goal name="WP_parameter peek.1" expl="1. precondition">
   <proof prover="0"><result status="valid" time="0.06" steps="79"/></proof>
   <proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -649,7 +651,8 @@
   <proof prover="3"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="WP_parameter pokethenpeek.9" expl="9. assertion">
-  <proof prover="0"><result status="valid" time="1.00" steps="341"/></proof>
+  <proof prover="7"><result status="valid" time="3.54" steps="212"/></proof>
+  <proof prover="8"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter pokethenpeek.10" expl="10. postcondition">
   <proof prover="0"><result status="valid" time="0.18" steps="94"/></proof>

examples/hashtbl_impl/why3session.xml

@@ -8,7 +8,7 @@
 <prover id="3" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../hashtbl_impl.mlw" expanded="true">
-<theory name="HashtblImpl" sum="cb495cd4418da69924cc3e0684ab0622" expanded="true">
+<theory name="HashtblImpl" sum="c0d16c1baac552217afa0ad022f76219" expanded="true">
  <goal name="bucket_bounds">
  <proof prover="0"><result status="valid" time="0.03" steps="16"/></proof>
  </goal>
@@ -236,7 +236,7 @@
   <proof prover="1"><result status="valid" time="0.08"/></proof>
   </goal>
   <goal name="WP_parameter add.4" expl="4. type invariant">
-  <proof prover="3" edited="hashtbl_impl_HashtblImpl_WP_parameter_add_1.v"><result status="valid" time="1.24"/></proof>
+  <proof prover="3" edited="hashtbl_impl_HashtblImpl_WP_parameter_add_1.v"><result status="valid" time="2.74"/></proof>
   </goal>
   <goal name="WP_parameter add.5" expl="5. type invariant">
   <transf name="inline_all">

examples/linear_probing/why3session.xml

@@ -12,7 +12,7 @@
  <proof prover="6"><result status="valid" time="0.01" steps="8"/></proof>
  </goal>
 </theory>
-<theory name="LinearProbing" sum="1cbb56a699a651dee5d971c187b7dba9" expanded="true">
+<theory name="LinearProbing" sum="0768e41be6d75fc5c0046b8691028429" expanded="true">
  <goal name="bucket_bounds">
  <proof prover="6"><result status="valid" time="0.02" steps="16"/></proof>
  </goal>
@@ -480,12 +480,12 @@
     <ip_library name="list"/>
     <ip_qualid name="list"/>
    </ts_pos>
-   <ts_pos name="ref" arity="1" id="4669"
+   <ts_pos name="ref" arity="1" id="4668"
     ip_theory="Ref">
     <ip_library name="ref"/>
     <ip_qualid name="ref"/>
    </ts_pos>
-   <ts_pos name="t" arity="0" id="6858"
+   <ts_pos name="t" arity="0" id="6857"
     ip_theory="LinearProbing">
     <ip_qualid name="t"/>
    </ts_pos>
@@ -574,26 +574,26 @@
     <ip_library name="map"/>
     <ip_qualid name="mixfix [&lt;-]"/>
    </ls_pos>
-   <ls_pos name="prefix !" id="4675"
+   <ls_pos name="prefix !" id="4674"
     ip_theory="Ref">
     <ip_library name="ref"/>
     <ip_qualid name="prefix !"/>
    </ls_pos>
-   <ls_pos name="set" id="4842"
+   <ls_pos name="set" id="4841"
     ip_theory="Array">
     <ip_library name="array"/>
     <ip_qualid name="set"/>
    </ls_pos>
-   <ls_pos name="mixfix [&lt;-]" id="4884"
+   <ls_pos name="mixfix [&lt;-]" id="4883"
     ip_theory="Array">
     <ip_library name="array"/>
     <ip_qualid name="mixfix [&lt;-]"/>
    </ls_pos>
-   <ls_pos name="numofd" id="6639"
+   <ls_pos name="numofd" id="6638"
     ip_theory="LinearProbing">
     <ip_qualid name="numofd"/>
    </ls_pos>
-   <ls_pos name="next" id="7479"
+   <ls_pos name="next" id="7478"
     ip_theory="LinearProbing">
     <ip_qualid name="next"/>
    </ls_pos>
@@ -801,16 +801,16 @@
     <ip_library name="map"/>
     <ip_qualid name="Select_neq"/>
    </pr_pos>
-   <pr_pos name="bucket_bounds" id="6300"
+   <pr_pos name="bucket_bounds" id="6299"
     ip_theory="LinearProbing">
     <ip_qualid name="bucket_bounds"/>
    </pr_pos>
-   <pr_pos name="numof_eq" id="6529"
+   <pr_pos name="numof_eq" id="6528"
     ip_theory="LinearProbing">
     <ip_qualid name="NumOfDummy"/>
     <ip_qualid name="numof_eq"/>
    </pr_pos>
-   <pr_pos name="dummy_const" id="6635"
+   <pr_pos name="dummy_const" id="6634"
     ip_theory="LinearProbing">
     <ip_qualid name="NumOfDummy"/>
     <ip_qualid name="dummy_const"/>
@@ -867,19 +867,19 @@
     <meta_arg_ls id="3301"/>
    </meta>
    <meta name="remove_logic">
-    <meta_arg_ls id="4675"/>
+    <meta_arg_ls id="4674"/>
    </meta>
    <meta name="remove_logic">
-    <meta_arg_ls id="4842"/>
+    <meta_arg_ls id="4841"/>
    </meta>
    <meta name="remove_logic">
-    <meta_arg_ls id="4884"/>
+    <meta_arg_ls id="4883"/>
    </meta>
    <meta name="remove_logic">
-    <meta_arg_ls id="6639"/>
+    <meta_arg_ls id="6638"/>
    </meta>
    <meta name="remove_logic">
-    <meta_arg_ls id="7479"/>
+    <meta_arg_ls id="7478"/>
    </meta>
    <meta name="remove_prop">
     <meta_arg_pr id="1607"/>
@@ -999,13 +999,13 @@
     <meta_arg_pr id="3323"/>
    </meta>
    <meta name="remove_prop">
-    <meta_arg_pr id="6300"/>
+    <meta_arg_pr id="6299"/>
    </meta>
    <meta name="remove_prop">
-    <meta_arg_pr id="6529"/>
+    <meta_arg_pr id="6528"/>
    </meta>
    <meta name="remove_prop">
-    <meta_arg_pr id="6635"/>
+    <meta_arg_pr id="6634"/>
    </meta>
    <meta name="remove_type">
     <meta_arg_ts id="2600"/>
@@ -1014,10 +1014,10 @@
     <meta_arg_ts id="2604"/>
    </meta>
    <meta name="remove_type">
-    <meta_arg_ts id="4669"/>
+    <meta_arg_ts id="4668"/>
    </meta>
    <meta name="remove_type">
-    <meta_arg_ts id="6858"/>
+    <meta_arg_ts id="6857"/>
    </meta>
    <goal name="WP_parameter copy.2" expl="2. type invariant">
    <proof prover="4" timelimit="5"><result status="valid" time="0.19"/></proof>
@@ -1025,7 +1025,7 @@
   </metas>
   </goal>
   <goal name="WP_parameter copy.3" expl="3. type invariant">
-  <proof prover="4"><result status="valid" time="1.26"/></proof>
+  <proof prover="4"><result status="valid" time="1.49"/></proof>
   </goal>
  </transf>
  </goal>
@@ -1338,7 +1338,7 @@
   <proof prover="6"><result status="valid" time="0.02" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter remove.5" expl="5. assertion">
-  <proof prover="0" timelimit="30"><result status="valid" time="23.31"/></proof>
+  <proof prover="0" timelimit="30"><result status="valid" time="20.59"/></proof>
   <proof prover="4" timelimit="30"><result status="valid" time="16.68"/></proof>
   </goal>
   <goal name="WP_parameter remove.6" expl="6. type invariant">

examples/max_matrix/why3session.xml

@@ -10,7 +10,7 @@
 </theory>
 <theory name="HashTable" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="MaxMatrixMemo" sum="cb32e0da8da5c9a9bc5507028cd7c2c1" expanded="true">
+<theory name="MaxMatrixMemo" sum="60d6a7dda5b713ca659b3a4deef37b09" expanded="true">
  <goal name="sum_ind">
  <proof prover="4" timelimit="47" memlimit="0"><result status="valid" time="0.15" steps="45"/></proof>
  </goal>

examples/patience/why3session.xml

@@ -142,7 +142,7 @@
  <proof prover="4"><result status="valid" time="0.02" steps="1"/></proof>
  </goal>
 </theory>
-<theory name="PatienceAbstract" sum="4bf96155881b495ecff2142b0df98c5d">
+<theory name="PatienceAbstract" sum="0440ad0575e0a9be9a69ae6d67427e6c">
  <goal name="WP_parameter play_card" expl="VC for play_card">
  <transf name="split_goal_wp">
   <goal name="WP_parameter play_card.1" expl="1. postcondition">

examples/pigeonhole/why3session.xml

@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
 <file name="../pigeonhole.mlw" expanded="true">
-<theory name="Pigeonhole" sum="a8dc8e1a803a05b577c3e88e7bd7151d" expanded="true">
+<theory name="Pigeonhole" sum="98798825bf4fb575a1fff7ac9ddb028b" expanded="true">
  <goal name="WP_parameter below" expl="VC for below" expanded="true">
  <proof prover="0"><result status="valid" time="0.01" steps="72"/></proof>
  </goal>

examples/remove_duplicate_hash/why3session.xml

@@ -8,7 +8,7 @@
 </theory>
 <theory name="MutableSet" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="RemoveDuplicate" sum="170bcbe1f13bb097aaf05b4437fedcda">
+<theory name="RemoveDuplicate" sum="e9ebf750d1da2bec48970f0169a0708b">
  <goal name="WP_parameter remove_duplicate" expl="VC for remove_duplicate">
  <transf name="split_goal_wp">
   <goal name="WP_parameter remove_duplicate.1" expl="1. index in array bounds">

examples/schorr_waite/why3session.xml

@@ -8,7 +8,7 @@
 <prover id="3" name="Alt-Ergo" version="1.00.prv" timelimit="10" steplimit="1" memlimit="4000"/>
 <prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="3500"/>
 <file name="../schorr_waite.mlw" expanded="true">
-<theory name="SchorrWaite" sum="0738a97b73d4ec8befdfe4cc5952fe94" expanded="true">
+<theory name="SchorrWaite" sum="fa7438e18ce047a276a62e848914f979" expanded="true">
  <goal name="WP_parameter tl_stackNodes" expl="VC for tl_stackNodes">
  <transf name="split_goal_wp">
   <goal name="WP_parameter tl_stackNodes.1" expl="1. postcondition">
@@ -48,12 +48,12 @@
   <proof prover="0" memlimit="4000"><result status="valid" time="0.01" steps="5"/></proof>
   </goal>
   <goal name="WP_parameter trans_path.4" expl="4. postcondition">
-  <proof prover="0" memlimit="4000"><result status="valid" time="0.46" steps="598"/></proof>
+  <proof prover="0" memlimit="4000"><result status="valid" time="0.61" steps="598"/></proof>
   <proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="0.51"/></proof>
   <proof prover="3"><result status="valid" time="0.07" steps="297"/></proof>
   </goal>
   <goal name="WP_parameter trans_path.5" expl="5. postcondition">
-  <proof prover="0" memlimit="4000"><result status="valid" time="0.66" steps="470"/></proof>
+  <proof prover="0" memlimit="4000"><result status="valid" time="0.66" steps="475"/></proof>
   </goal>
   <goal name="WP_parameter trans_path.6" expl="6. postcondition">
   <proof prover="0" memlimit="4000"><result status="valid" time="0.05" steps="101"/></proof>
@@ -166,7 +166,7 @@
   <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.33" expl="33. loop invariant preservation">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.34" expl="34. loop invariant preservation">
   <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -190,7 +190,7 @@
   <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.41" expl="41. loop invariant preservation">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.42" expl="42. loop invariant preservation">
   <proof prover="2"><result status="valid" time="0.05"/></proof>
@@ -354,16 +354,16 @@
    <goal name="WP_parameter schorr_waite.94.1" expl="1. loop invariant preservation">
    <transf name="split_goal_wp">
     <goal name="WP_parameter schorr_waite.94.1.1" expl="1. loop invariant preservation">
-    <proof prover="2"><result status="valid" time="0.98"/></proof>
+    <proof prover="2"><result status="valid" time="0.76"/></proof>
     </goal>
     <goal name="WP_parameter schorr_waite.94.1.2" expl="2. loop invariant preservation">
-    <proof prover="2"><result status="valid" time="1.01"/></proof>
+    <proof prover="2"><result status="valid" time="0.77"/></proof>
     </goal>
     <goal name="WP_parameter schorr_waite.94.1.3" expl="3. loop invariant preservation">
-    <proof prover="2"><result status="valid" time="1.00"/></proof>
+    <proof prover="2"><result status="valid" time="0.77"/></proof>
     </goal>
     <goal name="WP_parameter schorr_waite.94.1.4" expl="4. loop invariant preservation">
-    <proof prover="2"><result status="valid" time="0.95"/></proof>
+    <proof prover="2"><result status="valid" time="0.73"/></proof>
     </goal>
    </transf>
    </goal>
@@ -432,7 +432,7 @@
      <proof prover="2"><result status="valid" time="0.89"/></proof>
      </goal>
      <goal name="WP_parameter schorr_waite.109.1.1.2" expl="2. VC for schorr_waite">
-     <proof prover="2"><result status="valid" time="0.92"/></proof>
+     <proof prover="2"><result status="valid" time="0.72"/></proof>
      </goal>
     </transf>
     </goal>
@@ -609,13 +609,13 @@
   <proof prover="2"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.161" expl="161. loop invariant preservation">
-  <proof prover="2"><result status="valid" time="0.43"/></proof>
+  <proof prover="2"><result status="valid" time="0.27"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.162" expl="162. loop invariant preservation">
   <proof prover="2"><result status="valid" time="0.27"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.163" expl="163. loop invariant preservation">
-  <proof prover="0" timelimit="6"><result status="valid" time="1.32" steps="654"/></proof>
+  <proof prover="0" timelimit="6"><result status="valid" time="1.05" steps="654"/></proof>
   <proof prover="2"><result status="valid" time="0.13"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.164" expl="164. loop invariant preservation">
@@ -631,7 +631,7 @@
   <proof prover="2"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.168" expl="168. loop invariant preservation">
-  <proof prover="0" timelimit="6"><result status="valid" time="0.89" steps="386"/></proof>
+  <proof prover="0" timelimit="6"><result status="valid" time="0.62" steps="386"/></proof>
   <proof prover="2"><result status="valid" time="0.15"/></proof>
   </goal>
   <goal name="WP_parameter schorr_waite.169" expl="169. loop invariant preservation">
@@ -649,7 +649,7 @@
   <goal name="WP_parameter schorr_waite.173" expl="173. loop invariant preservation">
   <transf name="split_goal_wp">
    <goal name="WP_parameter schorr_waite.173.1" expl="1. loop invariant preservation">
-   <proof prover="2"><result status="valid" time="0.08"/></proof>
+   <proof prover="2"><result status="valid" time="0.20"/></proof>
    </goal>
    <goal name="WP_parameter schorr_waite.173.2" expl="2. loop invariant preservation">
    <proof prover="2"><result status="valid" time="0.08"/></proof>

examples/sudoku/why3session.xml

@@ -701,7 +701,7 @@
  <proof prover="4"><result status="valid" time="0.10" steps="48"/></proof>
  </goal>
 </theory>
-<theory name="Test" sum="af6a17d261da76da02f8f97ef561bb9c" expanded="true">
+<theory name="Test" sum="3d9a012589e18ca84e431bd224d427d3" expanded="true">
  <goal name="WP_parameter test0" expl="VC for test0">
  <proof prover="0"><result status="valid" time="0.02"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>

examples/sum_of_digits.mlw

@@ -76,6 +76,8 @@ module Euler290
     variant  { m }
   = if m = 0 then begin
       (* only n = 0 is possible *)
+      assert { power 10 m = 1 };
+      assert { numof a b 10 0 (power 10 m) = if sum_digits a + b = 0 then 1 else 0 };
       if sd a + b = 0 then 1 else 0
     end else begin
       let sum = ref 0 in

examples/sum_of_digits/why3session.xml

@@ -7,7 +7,7 @@
 <prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../sum_of_digits.mlw" expanded="true">
-<theory name="Euler290" sum="5950e38d51708bc5294e0e3fea4ec17f" expanded="true">
+<theory name="Euler290" sum="18226cdd8c439a37143a6081d0907d85" expanded="true">
  <goal name="Base">
  <proof prover="4" timelimit="10"><result status="valid" time="0.01" steps="10"/></proof>
  </goal>
@@ -22,43 +22,56 @@
  </goal>
  <goal name="WP_parameter f" expl="VC for f">
  <transf name="split_goal_wp">
-  <goal name="WP_parameter f.1" expl="1. precondition">
-  <proof prover="4"><result status="valid" time="0.03" steps="3"/></proof>
+  <goal name="WP_parameter f.1" expl="1. assertion">
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="WP_parameter f.2" expl="2. postcondition">
-  <proof prover="4"><result status="valid" time="0.18" steps="96"/></proof>
+  <goal name="WP_parameter f.2" expl="2. assertion">
+  <proof prover="1"><result status="valid" time="2.70"/></proof>
   </goal>
-  <goal name="WP_parameter f.3" expl="3. postcondition">
+  <goal name="WP_parameter f.3" expl="3. precondition">
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter f.4" expl="4. postcondition">
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter f.5" expl="5. postcondition">
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
   <proof prover="4"><result status="valid" time="0.02" steps="3"/></proof>
   </goal>
-  <goal name="WP_parameter f.4" expl="4. loop invariant init">
+  <goal name="WP_parameter f.6" expl="6. loop invariant init">
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   <proof prover="4"><result status="valid" time="0.03" steps="6"/></proof>
   </goal>
-  <goal name="WP_parameter f.5" expl="5. variant decrease">
+  <goal name="WP_parameter f.7" expl="7. variant decrease">
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
   <proof prover="4"><result status="valid" time="0.02" steps="7"/></proof>
   </goal>
-  <goal name="WP_parameter f.6" expl="6. precondition">
+  <goal name="WP_parameter f.8" expl="8. precondition">
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
   <proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
   </goal>
-  <goal name="WP_parameter f.7" expl="7. assertion">
+  <goal name="WP_parameter f.9" expl="9. assertion">
   <transf name="split_goal_wp">
-   <goal name="WP_parameter f.7.1" expl="1. VC for f">
+   <goal name="WP_parameter f.9.1" expl="1. VC for f">
+   <proof prover="1"><result status="valid" time="0.04"/></proof>
    <proof prover="4"><result status="valid" time="0.16" steps="38"/></proof>
    </goal>
-   <goal name="WP_parameter f.7.2" expl="2. VC for f">
+   <goal name="WP_parameter f.9.2" expl="2. VC for f">
+   <proof prover="1"><result status="valid" time="0.03"/></proof>
    <proof prover="4"><result status="valid" time="0.07" steps="26"/></proof>
    </goal>
-   <goal name="WP_parameter f.7.3" expl="3. VC for f">
+   <goal name="WP_parameter f.9.3" expl="3. VC for f">
    <proof prover="4"><result status="valid" time="0.01" steps="14"/></proof>
    </goal>
   </transf>
   </goal>
-  <goal name="WP_parameter f.8" expl="8. loop invariant preservation">
+  <goal name="WP_parameter f.10" expl="10. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.02"/></proof>
   <proof prover="1"><result status="valid" time="0.03"/></proof>
   <proof prover="4"><result status="valid" time="0.02" steps="16"/></proof>
   </goal>
-  <goal name="WP_parameter f.9" expl="9. postcondition">
+  <goal name="WP_parameter f.11" expl="11. postcondition">
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
   <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
  </transf>

examples/vstte12_bfs/why3session.xml

@@ -11,7 +11,7 @@
 <prover id="8" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
 <file name="../vstte12_bfs.mlw" expanded="true">
-<theory name="Graph" sum="c68d6882c9dfec50df4fa4cb8d22f0b0" expanded="true">
+<theory name="Graph" sum="143fe0ebe09e8c4b0c8df4088f6fc209" expanded="true">
  <goal name="path_nonneg">
  <transf name="induction_pr">
   <goal name="path_nonneg.1" expl="1.">
@@ -45,7 +45,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="BFS" sum="1c4e9affeb06eecd52118ffdf9845b83" expanded="true">
+<theory name="BFS" sum="99c8c398973756db21fb40314f8f11cb" expanded="true">
  <goal name="WP_parameter fill_next" expl="VC for fill_next">
  <transf name="split_goal_wp">
   <goal name="WP_parameter fill_next.1" expl="1. loop invariant init">

examples/vstte12_ring_buffer/why3session.xml

@@ -176,12 +176,12 @@
      <ip_library name="Mark"/>
      <ip_qualid name="&apos;mark"/>
     </ts_pos>
-    <ts_pos name="array" arity="1" id="4401"
+    <ts_pos name="array" arity="1" id="4400"
      ip_theory="Array">
      <ip_library name="array"/>
      <ip_qualid name="array"/>
     </ts_pos>
-    <ts_pos name="buffer" arity="1" id="5875"
+    <ts_pos name="buffer" arity="1" id="5874"
      ip_theory="RingBuffer">
      <ip_qualid name="buffer"/>
     </ts_pos>
@@ -246,36 +246,36 @@
      <ip_library name="map"/>
      <ip_qualid name="mixfix [&lt;-]"/>
     </ls_pos>
-    <ls_pos name="infix ++" id="3730"
+    <ls_pos name="infix ++" id="3729"
      ip_theory="Append">
      <ip_library name="list"/>
      <ip_qualid name="infix ++"/>
     </ls_pos>
-    <ls_pos name="get" id="4409"
+    <ls_pos name="get" id="4408"
      ip_theory="Array">
      <ip_library name="array"/>
      <ip_qualid name="get"/>
     </ls_pos>
-    <ls_pos name="set" id="4424"
+    <ls_pos name="set" id="4423"
      ip_theory="Array">
      <ip_library name="array"/>
      <ip_qualid name="set"/>
     </ls_pos>
-    <ls_pos name="mixfix []" id="4449"
+    <ls_pos name="mixfix []" id="4448"
      ip_theory="Array">
      <ip_library name="array"/>
      <ip_qualid name="mixfix []"/>
     </ls_pos>
-    <ls_pos name="mixfix [&lt;-]" id="4466"
+    <ls_pos name="mixfix [&lt;-]" id="4465"
      ip_theory="Array">
      <ip_library name="array"/>
      <ip_qualid name="mixfix [&lt;-]"/>
     </ls_pos>
-    <ls_pos name="size" id="5889"
+    <ls_pos name="size" id="5888"
      ip_theory="RingBuffer">
      <ip_qualid name="size"/>
     </ls_pos>
-    <ls_pos name="length" id="5898"
+    <ls_pos name="length" id="5897"
      ip_theory="RingBuffer">
      <ip_qualid name="length"/>
     </ls_pos>
@@ -403,47 +403,47 @@
      <ip_library name="map"/>
      <ip_qualid name="Select_neq"/>
     </pr_pos>