update prover identifiers in Coq proofs

examples/hoare_logic/blocking_semantics/blocking_semantics_WP_wp_conj_1.v

@@ -480,7 +480,7 @@ Unset Implicit Arguments.
 Require Why3.
 Ltac ae := why3 "alt-ergo" timelimit 2.
 Ltac ae10 := why3 "alt-ergo" timelimit 10.
-Ltac cvc10 := why3 "cvc3-2.4" timelimit 10.
+Ltac cvc10 := why3 "cvc3" timelimit 10.
 
 (* Why3 goal *)
 Theorem wp_conj : forall (sigma:(map Z value)) (pi:(list (Z* value)%type))

examples/hoare_logic/blocking_semantics/blocking_semantics_WP_wp_reduction_1.v

@@ -561,7 +561,7 @@ Axiom wp_conj : forall (sigma:(map ident value)) (pi:(list (ident*
 Require Why3.
 Ltac ae := why3 "alt-ergo" timelimit 2.
 Ltac ae10 := why3 "alt-ergo" timelimit 10.
-Ltac cvc10 := why3 "cvc3-2.4" timelimit 10.
+Ltac cvc10 := why3 "cvc3" timelimit 10.
 
 (* Why3 goal *)
 Theorem wp_reduction : forall (sigma:(map ident value)) (sigma':(map ident

examples/programs/bellman_ford/bellman_ford_Graph_long_path_decomposition_pigeon1_1.v

@@ -256,7 +256,7 @@ Theorem long_path_decomposition_pigeon1 : forall (l:(list vertex))
 
 Require Why3.
 Ltac ae := why3 "alt-ergo".
-Ltac cvc := why3 "cvc3-2.4".
+Ltac cvc := why3 "cvc3".
 
 intros l v H0.
 induction H0.

examples/programs/bellman_ford/bellman_ford_Graph_long_path_decomposition_pigeon3_1.v

@@ -271,7 +271,7 @@ Theorem long_path_decomposition_pigeon3 : forall (l:(list vertex))
 
 Require Why3.
 Ltac ae := why3 "alt-ergo".
-Ltac cvc := why3 "cvc3-2.4".
+Ltac cvc := why3 "cvc3".
 
 intros l v H1.
 destruct H1 as (e & l1 & l2 & l3 & H1).

examples/programs/bellman_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_15.v

@@ -417,7 +417,7 @@ intros (h4, h5).
 destruct (get m u) as [] _eqn. 2: intuition.
 destruct (get m v) as [] _eqn.
 intros hlt. apply key_lemma_1 with v z0.
-why3 "z3-3".
+why3 "z3".
 assert (hu: exists lu: list vertex, path s lu u /\ path_weight lu u = z) by ae.
 destruct hu as (lu, (hu1, hu2)).
 exists (infix_plpl lu (Cons u Nil)); ae.

examples/programs/bellman_ford/bf_WP_BellmanFord_WP_parameter_bellman_ford_17.v

@@ -438,7 +438,7 @@ Axiom key_lemma_2 : forall (m:(map vertex t)), (inv1 m (cardinal vertices)
   forall (v:vertex), ~ (negative_cycle v)).
 
 Require Import Why3.
-Ltac Z3 := why3 "z3-3".
+Ltac Z3 := why3 "z3".
 Ltac ae := why3 "alt-ergo".
 
 (* Why3 goal *)
@@ -498,7 +498,7 @@ destruct (get m1 v) as [] _eqn; auto.
 intros l hpath hlength.
 destruct (path_right_inversion s v l hpath) as [(h1,h2) | (y, (l', (h1, (h2, h3))))].
 (* Nil *)
-subst. simpl. why3 "cvc3-2.4".
+subst. simpl. why3 "cvc3".
 (* Cons *)
 rewrite h3; rewrite path_weight_right_extension.
 generalize (H6 v H7); clear H6.

examples/programs/bellman_ford/bf_WP_BellmanFord_key_lemma_2_1.v

@@ -435,7 +435,7 @@ Definition inv2(m:(map vertex t)) (via:(set1 (vertex* vertex)%type)): Prop :=
 
 Require Import Why3.
 Ltac ae := why3 "alt-ergo" timelimit 30.
-Ltac Z3 := why3 "z3-3" timelimit 10.
+Ltac Z3 := why3 "z3" timelimit 10.
 
 Lemma length_nonneg: forall a, forall l: list a, (length l >= 0)%Z.
 induction l; ae.

examples/programs/distance/distance_Distance_WP_parameter_distance_1.v

@@ -134,12 +134,12 @@ generalize (h10 k h). intros h10k.
 assert (case: (j < get g1 k \/ j = get g1 k \/ j > get g1 k)%Z) by omega.
 destruct case.
 (* j < g[k] *)
-why3 "z3-3" timelimit 5.
+why3 "z3" timelimit 5.
 destruct H5.
 (* j = g[k] *)
 ae.
 (* j > g[k] *)
-why3 "z3-3" timelimit 3.
+why3 "z3" timelimit 3.
 (* k = 0 *)
 ae.
 Qed.

examples/programs/fibonacci/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
 <why3session
- name="examples/programs/fibonacci/why3session.xml" shape_version="2">
+ name="programs/fibonacci/why3session.xml" shape_version="2">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -36,7 +36,7 @@
   expanded="true">
   <theory
    name="Fibonacci"
-   locfile="examples/programs/fibonacci/../fibonacci.mlw"
+   locfile="programs/fibonacci/../fibonacci.mlw"
    loclnum="2" loccnumb="7" loccnume="16"
    verified="true"
    expanded="true">
@@ -45,13 +45,13 @@
   </theory>
   <theory
    name="FibonacciTest"
-   locfile="examples/programs/fibonacci/../fibonacci.mlw"
+   locfile="programs/fibonacci/../fibonacci.mlw"
    loclnum="14" loccnumb="7" loccnume="20"
    verified="true"
    expanded="false">
    <goal
     name="isfib_2_1"
-    locfile="examples/programs/fibonacci/../fibonacci.mlw"
+    locfile="programs/fibonacci/../fibonacci.mlw"
     loclnum="18" loccnumb="8" loccnume="17"
     sum="53cb43c962b6ac473353e3b02dc4b67b"
     proved="true"
@@ -68,7 +68,7 @@
    </goal>
    <goal
     name="isfib_6_8"
-    locfile="examples/programs/fibonacci/../fibonacci.mlw"
+    locfile="programs/fibonacci/../fibonacci.mlw"
     loclnum="19" loccnumb="8" loccnume="17"
     sum="23ec2eb87c0bebe1406c9b91f62e2d92"
     proved="true"
@@ -85,7 +85,7 @@
    </goal>
    <goal
     name="not_isfib_2_2"
-    locfile="examples/programs/fibonacci/../fibonacci.mlw"
+    locfile="programs/fibonacci/../fibonacci.mlw"
     loclnum="21" loccnumb="8" loccnume="21"
     sum="f3cd71efc59ece547b8cfe0932c063ca"
     proved="true"
@@ -135,13 +135,13 @@
   </theory>
   <theory
    name="FibonacciLinear"
-   locfile="examples/programs/fibonacci/../fibonacci.mlw"
+   locfile="programs/fibonacci/../fibonacci.mlw"
    loclnum="25" loccnumb="7" loccnume="22"
    verified="true"
    expanded="false">
    <goal
     name="WP_parameter fib"
-    locfile="examples/programs/fibonacci/../fibonacci.mlw"
+    locfile="programs/fibonacci/../fibonacci.mlw"
     loclnum="31" loccnumb="6" loccnume="9"
     expl="parameter fib"
     sum="0524e9e40b90c0c213c0df1110b389f1"
@@ -162,7 +162,7 @@
   </theory>
   <theory
    name="Mat22"
-   locfile="examples/programs/fibonacci/../fibonacci.mlw"
+   locfile="programs/fibonacci/../fibonacci.mlw"
    loclnum="46" loccnumb="7" loccnume="12"
    verified="true"
    expanded="true">
@@ -171,16 +171,16 @@
   </theory>
   <theory
    name="FibonacciLogarithmic"
-   locfile="examples/programs/fibonacci/../fibonacci.mlw"
+   locfile="programs/fibonacci/../fibonacci.mlw"
    loclnum="68" loccnumb="7" loccnume="27"
    verified="true"
    expanded="true">
    <goal
     name="WP_parameter logfib"
-    locfile="examples/programs/fibonacci/../fibonacci.mlw"
+    locfile="programs/fibonacci/../fibonacci.mlw"
     loclnum="82" loccnumb="10" loccnume="16"
     expl="parameter logfib"
-    sum="3966dacbc1855018004e996b874f27fa"
+    sum="49924bf2200f24435af2c0570880fc85"
     proved="true"
     expanded="true"
     shape="iainfix =V0c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FAainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix &gt;=V0c0F">
@@ -192,10 +192,10 @@
      expanded="true">
      <goal
       name="WP_parameter logfib.1"
-      locfile="examples/programs/fibonacci/../fibonacci.mlw"
+      locfile="programs/fibonacci/../fibonacci.mlw"
       loclnum="82" loccnumb="10" loccnume="16"
       expl="normal postcondition"
-      sum="adf3fda094b1f16d576b23cf13147c8d"
+      sum="00aa5f8fcdddef70d5665548b1986d96"
       proved="true"
       expanded="true"
       shape="ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Iainfix =V0c0Iainfix &gt;=V0c0F">
@@ -236,10 +236,10 @@
      </goal>
      <goal
       name="WP_parameter logfib.2"
-      locfile="examples/programs/fibonacci/../fibonacci.mlw"
+      locfile="programs/fibonacci/../fibonacci.mlw"
       loclnum="82" loccnumb="10" loccnume="16"
       expl="variant decreases"
-      sum="4464035e38e634573f8cf479606f0013"
+      sum="01a989f467c67e8551c8707a051cf515"
       proved="true"
       expanded="true"
       shape="ainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
@@ -251,15 +251,15 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter logfib.3"
-      locfile="examples/programs/fibonacci/../fibonacci.mlw"
+      locfile="programs/fibonacci/../fibonacci.mlw"
       loclnum="82" loccnumb="10" loccnume="16"
       expl="precondition"
-      sum="914eb29f581e4f81f1dc88e3cd6a2125"
+      sum="ec53c68db6b793ce5dd13c260a850beb"
       proved="true"
       expanded="true"
       shape="ainfix &gt;=adivV0c2c0Iainfix =V0c0NIainfix &gt;=V0c0F">
@@ -284,10 +284,10 @@
      </goal>
      <goal
       name="WP_parameter logfib.4"
-      locfile="examples/programs/fibonacci/../fibonacci.mlw"
+      locfile="programs/fibonacci/../fibonacci.mlw"
       loclnum="82" loccnumb="10" loccnume="16"
       expl="normal postcondition"
-      sum="c8a4a4717b459e34b8d3a05ff9c7fb31"
+      sum="8054b2592b4645e2207abf30a53e8434"
       proved="true"
       expanded="false"
       shape="iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FIainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
@@ -300,16 +300,16 @@
        edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.62"/>
+       <result status="valid" time="0.63"/>
       </proof>
      </goal>
     </transf>
    </goal>
    <goal
     name="fib_m"
-    locfile="examples/programs/fibonacci/../fibonacci.mlw"
+    locfile="programs/fibonacci/../fibonacci.mlw"
     loclnum="105" loccnumb="8" loccnume="13"
-    sum="e8605b6494a93cb6a637cf1c1f211395"
+    sum="3b9e61634104ae731da8aac4b1e65d66"
     proved="true"
     expanded="true"
     shape="ainfix =afibV0aa21V1Aainfix =afibainfix +V0c1aa11V1Lapoweram1110V0Iainfix &gt;=V0c0F">
@@ -320,15 +320,15 @@
      edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.51"/>
+     <result status="valid" time="0.50"/>
     </proof>
    </goal>
    <goal
     name="WP_parameter fibo"
-    locfile="examples/programs/fibonacci/../fibonacci.mlw"
+    locfile="programs/fibonacci/../fibonacci.mlw"
     loclnum="109" loccnumb="6" loccnume="10"
     expl="parameter fibo"
-    sum="734efa163a10e0cf86c5d09f85bfb2e7"
+    sum="de5a7016f6c65e44ea77685242059e4e"
     proved="true"
     expanded="false"
     shape="ainfix =V2afibV0Iainfix =apoweramk tc1c1c1c0V0amk tainfix +V1V2V2V2V1FAainfix &gt;=V0c0Iainfix &gt;=V0c0F">
@@ -348,7 +348,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
   </theory>

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_prefix_1.v

@@ -90,7 +90,7 @@ Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z))
 Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
   t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
 
-Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
+Require Import Why3. Ltac z := why3 "z3" timelimit 5.
 
 (* Why3 goal *)
 Theorem depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_subtree_1.v

@@ -97,7 +97,7 @@ Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list
 Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
   t) = (depths d2 t)) -> (d1 = d2).
 
-Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
+Require Import Why3. Ltac z := why3 "z3" timelimit 5.
 
 (* Why3 goal *)
 Theorem depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z) (s1:(list

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_unique2_1.v

@@ -97,7 +97,7 @@ Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
 Axiom depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z) (s1:(list
   Z)), ((infix_plpl (depths d1 t1) s1) = (depths d2 t2)) -> (d2 <= d1)%Z.
 
-Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
+Require Import Why3. Ltac z := why3 "z3" timelimit 5.
 
 (* Why3 goal *)
 Theorem depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z),

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_WP_parameter_tc_1.v

@@ -177,7 +177,7 @@ Axiom main_lemma : forall (l:(list (Z* tree)%type)) (d1:Z) (d2:Z) (t1:tree)
   (t2:tree), (~ (d1 = d2)) -> ((g (reverse (Cons (d1, t1) l))) ->
   (g (reverse (Cons (d2, t2) (Cons (d1, t1) l))))).
 
-Require Import Why3. Ltac z := why3 "z3-3".
+Require Import Why3. Ltac z := why3 "z3".
 
 (* Why3 goal *)
 Theorem WP_parameter_tc : forall (left1:(list (Z* tree)%type)),

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_WP_parameter_tc_2.v

@@ -180,7 +180,7 @@ Axiom main_lemma : forall (l:(list (Z* tree)%type)) (d1:Z) (d2:Z) (t1:tree)
   (t2:tree), (~ (d1 = d2)) -> ((g (reverse (Cons (d1, t1) l))) ->
   (g (reverse (Cons (d2, t2) (Cons (d1, t1) l))))).
 
-Require Import Why3. Ltac z := why3 "z3-3".
+Require Import Why3. Ltac z := why3 "z3".
 
 (* Why3 goal *)
 Theorem WP_parameter_tc : forall (left1:(list (Z* tree)%type)),

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_WP_parameter_tc_4.v

@@ -180,7 +180,7 @@ Axiom main_lemma : forall (l:(list (Z* tree)%type)) (d1:Z) (d2:Z) (t1:tree)
   (t2:tree), (~ (d1 = d2)) -> ((g (reverse (Cons (d1, t1) l))) ->
   (g (reverse (Cons (d2, t2) (Cons (d1, t1) l))))).
 
-Require Import Why3. Ltac z := why3 "z3-3".
+Require Import Why3. Ltac z := why3 "z3".
 
 (* Why3 goal *)
 Theorem WP_parameter_tc : forall (left1:(list (Z* tree)%type)),

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_WP_parameter_tc_5.v

@@ -200,7 +200,7 @@ Axiom main_lemma : forall (l:(list (Z* tree)%type)) (d1:Z) (d2:Z) (t1:tree)
   | Leaf => True
   end -> (g (Cons (d2, t2) (Cons (d1, t1) l))))).
 
-Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
+Require Import Why3. Ltac z := why3 "z3" timelimit 5.
 
 (* Why3 goal *)
 Theorem WP_parameter_tc : forall (left1:(list (Z* tree)%type)),

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_g_append_1.v

@@ -187,7 +187,7 @@ Inductive g : (list (Z* tree)%type) -> Prop :=
       tree)%type)), (greedy d1 d2 t2) -> ((g (Cons (d1, t1) l)) -> (g (Cons (
       d2, t2) (Cons (d1, t1) l)))).
 
-Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
+Require Import Why3. Ltac z := why3 "z3" timelimit 5.
 
 (* Why3 goal *)
 Theorem g_append : forall (l1:(list (Z* tree)%type)) (l2:(list (Z*

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_g_tail_1.v

@@ -170,7 +170,7 @@ Inductive g : (list (Z* tree)%type) -> Prop :=
   | Gtwo : forall (d:Z) (t:tree) (l:(list (Z* tree)%type)), (greedy d t l) ->
       ((g l) -> (g (Cons (d, t) l))).
 
-Require Import Why3. Ltac z := why3 "z3-3".
+Require Import Why3. Ltac z := why3 "z3".
 
 (* Why3 goal *)
 Theorem g_tail : forall (l:(list (Z* tree)%type)) (d:Z) (t:tree),

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_main_lemma_1.v

@@ -194,7 +194,7 @@ Axiom right_nil : forall (l:(list (Z* tree)%type)), (2%Z <= (length l))%Z ->
   ((g l) -> forall (t:tree), ~ ((forest_depths (reverse l)) = (depths 0%Z
   t))).
 
-Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
+Require Import Why3. Ltac z := why3 "z3" timelimit 5.
 
 (*
 Lemma key_lemma:

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v

@@ -7,21 +7,6 @@ Require int.Int.
 (* Why3 assumption *)
 Definition unit  := unit.
 
-Parameter qtmark : Type.
-
-Parameter at1: forall (a:Type), a -> qtmark -> a.
-Implicit Arguments at1.
-
-Parameter old: forall (a:Type), a -> a.
-Implicit Arguments old.
-
-(* Why3 assumption *)
-Definition implb(x:bool) (y:bool): bool := match (x,
-  y) with
-  | (true, false) => false
-  | (_, _) => true
-  end.
-
 (* Why3 assumption *)
 Inductive list (a:Type) :=
   | Nil : list a
@@ -119,7 +104,7 @@ Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
   t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
 
 (* Why3 assumption *)
-Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x <  y)%Z.
+Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
 
 (* Why3 assumption *)
 Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop :=
@@ -160,15 +145,6 @@ Axiom forest_depths_append : forall (f1:(list (Z* tree)%type)) (f2:(list (Z*
   tree)%type)), ((forest_depths (infix_plpl f1
   f2)) = (infix_plpl (forest_depths f1) (forest_depths f2))).
 
-(* Why3 assumption *)
-Set Implicit Arguments.
-Fixpoint only_leaf(l:(list (Z* tree)%type)) {struct l}: Prop :=
-  match l with
-  | Nil => True
-  | (Cons (_, t) r) => (t = Leaf) /\ (only_leaf r)
-  end.
-Unset Implicit Arguments.
-
 (* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint greedy(d:Z) (d1:Z) (t1:tree) {struct t1}: Prop := (~ (d = d1)) /\
@@ -190,7 +166,7 @@ Inductive g : (list (Z* tree)%type) -> Prop :=
 Axiom g_append : forall (l1:(list (Z* tree)%type)) (l2:(list (Z*
   tree)%type)), (g (infix_plpl l1 l2)) -> (g l1).
 
-Require Import Why3. Ltac z := why3 "z3-3" timelimit 5.
+Require Import Why3. Ltac z := why3 "z3" timelimit 5.
 Ltac ae := why3 "alt-ergo".
 
 Lemma depths_length: forall t d, (length (depths d t) >= 1)%Z.
@@ -208,7 +184,7 @@ Qed.
 Lemma g_tail : forall (l1:(list (Z* tree)%type)) (l2:(list (Z*
   tree)%type)), (g (infix_plpl l1 l2)) -> (g l2).
 induction l1; simpl; auto.
-z.
+ae.
 Qed.
 
 Theorem key_lemma : forall t l d d1 t1 s, (d < d1)%Z ->
@@ -241,7 +217,7 @@ assert (case: (d2 < d1 \/ d1 < d2)%Z) by omega. destruct case as [case|case].
 assert (L0: (forall t2 d1 d2, greedy d1 d2 t2 -> d2 < d1 ->
    match depths d2 t2 with Cons x _ => x < d1 | Nil  => False end)%Z).
   induction t0.
-  z.
+  ae.
   simpl.
   clear IHt0_2.
   intros d0 d3 (diseq, gr) lt.
@@ -343,7 +319,7 @@ generalize eq; clear eq.
 replace (depths d t) with (infix_plpl (depths d t) Nil) by z.
 apply key_lemma; auto.
 simpl in H.
-z.
+ae.
 Qed.
 
 

examples/programs/vstte12_tree_reconstruction/why3session.xml

@@ -65,7 +65,7 @@
      edited="vstte12_tree_reconstruction_Tree_depths_unique_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.51"/>
+     <result status="valid" time="0.52"/>
     </proof>
    </goal>
    <goal
@@ -83,7 +83,7 @@
      edited="vstte12_tree_reconstruction_Tree_depths_prefix_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.62"/>
+     <result status="valid" time="0.70"/>
     </proof>
    </goal>
    <goal
@@ -100,7 +100,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
@@ -118,7 +118,7 @@
      edited="vstte12_tree_reconstruction_Tree_depths_subtree_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.92"/>
+     <result status="valid" time="0.90"/>
     </proof>
    </goal>
    <goal
@@ -136,7 +136,7 @@
      edited="vstte12_tree_reconstruction_Tree_depths_unique2_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.80"/>
+     <result status="valid" time="0.83"/>
     </proof>
    </goal>
   </theory>
@@ -198,7 +198,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="1.37"/>
+       <result status="valid" time="1.18"/>
       </proof>
      </goal>
      <goal
@@ -316,7 +316,7 @@
        edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_rec_3.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.58"/>
+       <result status="valid" time="0.63"/>
       </proof>
      </goal>
      <goal
@@ -337,7 +337,7 @@
        edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_rec_4.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.55"/>
+       <result status="valid" time="0.52"/>
       </proof>
      </goal>
     </transf>
@@ -395,7 +395,7 @@
        edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_3.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.51"/>
+       <result status="valid" time="0.53"/>
       </proof>
      </goal>
      <goal
@@ -416,7 +416,7 @@
        edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_4.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.50"/>
+       <result status="valid" time="0.48"/>
       </proof>
      </goal>
     </transf>
@@ -482,7 +482,7 @@
        edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness_4.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.46"/>
+       <result status="valid" time="0.47"/>
       </proof>
      </goal>
     </transf>
@@ -505,7 +505,7 @@
      edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness2_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.63"/>
+     <result status="valid" time="0.67"/>
     </proof>
    </goal>
   </theory>
@@ -607,7 +607,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.07"/>
+       <result status="valid" time="0.06"/>
       </proof>
      </goal>
      <goal
@@ -667,7 +667,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
     </transf>
@@ -694,7 +694,7 @@
      edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.49"/>
+     <result status="valid" time="0.47"/>
     </proof>
    </goal>
    <goal
@@ -712,7 +712,7 @@
      edited="vstte12_tree_reconstruction_WP_ZipperBased_g_append_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.02"/>
+     <result status="valid" time="1.05"/>
     </proof>
    </goal>
    <goal
@@ -730,7 +730,7 @@
      edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="7.70"/>
+     <result status="valid" time="5.94"/>
     </proof>
    </goal>
    <goal
@@ -798,7 +798,7 @@
          memlimit="0"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.10"/>
+         <result status="valid" time="0.09"/>
         </proof>
        </goal>
        <goal
@@ -860,7 +860,7 @@
        memlimit="0"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.88"/>
+       <result status="valid" time="0.72"/>
       </proof>
      </goal>
      <goal
@@ -881,7 +881,7 @@
        edited="vstte12_tree_reconstruction_WP_ZipperBased_WP_parameter_tc_2.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.84"/>
+       <result status="valid" time="0.85"/>
       </proof>
      </goal>
      <goal
@@ -916,7 +916,7 @@
          memlimit="0"
          obsolete="false"
          archived="false">