insert and riser work

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/contracts@12648 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

9 files changed, 660 insertions, 313 deletions

diff --git a/verify/esc.ml b/verify/esc.ml
index 8a1e8b387e..de401adb60 100644
--- a/verify/esc.ml
+++ b/verify/esc.ml
@@ -198,10 +198,10 @@ type outname = Path.t
 
 (* Types for continuation *)
 
-type cont =  (* e a1 HOLE an *)
-    Cargs of ThmEnv.t (* same env for all args *) 
-          * inexp (* function *)
-          * (inexp option * optional) list  (* args done *)
+type cont =  (* f a1 HOLE an *)
+    Cargs of ThmEnv.t (* env for undone args *) 
+          * outexp (* function *)
+          * (outexp option * optional) list  (* args done *)
           * optional  (* for current arg being simplified *)
           * (inexp option * optional) list  (*args not done *) 
           * type_expr (* result type *) 
@@ -212,16 +212,21 @@ type cont =  (* e a1 HOLE an *)
   | CLam of expression (* original expression *)
           * pattern *partial (* \x.HOLE *)
   | Cprim of (inexp option * optional) list * type_expr (* op HOLE e2 *)
+  | Ccons of ThmEnv.t * expression * (* original expression *)
+	     Path.t * constructor_description *
+	     outexp list * inexp list (* K(HOLE,e) *)
   | Cin of rec_flag * (pattern * outexp) list (* let x = e1 in HOLE *)
             (* let x1 = a1 
                    x = HOLE
 	           x2 = a2
                in e2 *)
-  | Clet of rec_flag * (pattern * outexp) list *
+  | Clet of ThmEnv.t * rec_flag * (pattern * outexp) list *
 	     pattern * (pattern * inexp) list * inexp 
   | Cmatch of (ThmEnv.t * expression (* original env and expression *)
             * inalt list * partial) (* match HOLE with x alts *)
   | Cif of (ThmEnv.t * expression * expression option) (* if HOLE then e1 else e2 *)
+  | Cthen of (ThmEnv.t * outexp * inexp option) (* if a0 then HOLE else e2 *)
+  | Celse of (outexp * outexp) (* if a0 then a1 else HOLE *)
   | Ctry of inalt list
 
 (* Symbolically simplify pure expression in Typedtree.expression *)
@@ -243,18 +248,25 @@ let is_contract_exception e = match e.exp_desc with
    the senv contains both the mapping from variable to value and 
    the logical store  *)
 let rec simpl_expr (senv : ThmEnv.t) (exp : expression) (k: cont list) : expression =
-  (* print_string "***esc.simpl_expr: \n"; print_expression exp; print_string "\n"; *)
+  trace "***esc.simpl_expr" print_expression exp;
   let mkexp desc = {exp with exp_desc = desc} in          
   match exp.exp_desc with  
-  | Texp_constant (c) -> rebuild senv exp k
-  | Texp_bad (bl) -> rebuild senv exp k
-  | Texp_unr (bl) -> rebuild senv exp k
+  | Texp_constant (c) -> rebuild exp k
+  | Texp_bad (bl) -> rebuild exp k
+  | Texp_unr (bl) -> rebuild exp k
   | Texp_ident (path, vdesc) -> 
       begin match path with
 	| Pident id -> 
-	    let aval = lookup_senv id senv in
-            rebuildVar senv (id, exp) aval k
-	| _ -> rebuild senv exp k
+	    begin
+	      let aval = lookup_senv id senv in
+	      match aval with
+	      | NoVal -> if depth senv = 1
+	                 then rebuild (try lookup_nonrec_env id senv
+                                       with Not_found -> exp) k
+		         else rebuild exp k
+	      | _ -> rebuildVar (id, exp) aval k
+	    end
+	| _ -> rebuild exp k
       end
   | Texp_function (pat_expr_list, ptial) ->
         (* NEW: we generate logic v : <type of v> 
@@ -264,7 +276,7 @@ let rec simpl_expr (senv : ThmEnv.t) (exp : expression) (k: cont list) : express
                        let env1 = add_tasks senv (bound_vars_to_logic p) in
 		       (p, simpl_expr env1 e []))
                        pat_expr_list in
-      rebuild senv {exp with exp_desc = Texp_function (simpl_list, ptial)} k
+      rebuild {exp with exp_desc = Texp_function (simpl_list, ptial)} k
   | Texp_apply (e1, eopt_optl_list) ->
       (* A-normalize the arguments *)
      let rec genLet xs = match xs with
@@ -291,14 +303,16 @@ let rec simpl_expr (senv : ThmEnv.t) (exp : expression) (k: cont list) : express
      let (args, p_e_list) = genLet eopt_optl_list in
      begin match p_e_list with
      | [] ->  
-	 simpl_expr senv e1 (Capp (senv, [], eopt_optl_list, exp.exp_type)::k) 
+	 simpl_expr senv e1 (Capp (senv, [], args, exp.exp_type)::k) 
      | _ -> 
 	 simpl_expr senv ({exp with exp_desc = Texp_let (Nonrecursive, p_e_list, 
 	     	          {exp with exp_desc = Texp_apply(e1, args)})}) k
      end
   | Texp_match (e0, pat_expr_list, ptial) ->       
       begin match k with
-      | (Capp (env, [], nds, res_type) :: k1) ->  (* [matchR] *)
+      | (Capp (env, [], nds, res_type) :: k1) ->  
+          (* (match e0 with pi -> ei) val ==> [matchL] 
+             match e0 with pi -> ei val                *)
           let p_e_list = List.map (fun (p,e) -> (p, 
                          { exp_desc = Texp_apply(e, nds);
                            exp_loc  = e.exp_loc;
@@ -308,33 +322,33 @@ let rec simpl_expr (senv : ThmEnv.t) (exp : expression) (k: cont list) : express
                          pat_expr_list in
 	  let expr1 = {exp with exp_desc = Texp_match (e0, p_e_list, ptial)} in
           simpl_expr senv expr1 k1
-      | (Clet (rflag, ds, p, uds, e2) :: k1) -> 
+      | (Clet (env, rflag, ds, p, uds, e2) :: k1) -> 
         (* let x = (match e0 with K x -> ei) in e2  ==>  [let-match]
 	   match e0 with K x -> let x = ei in e2 *)
-	   if rflag = Nonrecursive then
+	   begin match rflag with
+           | Nonrecursive ->
 	   let rhs = {exp with exp_desc = Texp_match(e0, 
 			     List.map (fun (pi,ei) -> (pi, {ei with exp_desc = 
 			 Texp_let (rflag, (p,ei)::uds, e2)})) pat_expr_list, ptial)}
            in simpl_expr senv rhs (Cin (rflag, ds)::k1)
-	  else simpl_expr senv e0 (Cmatch (senv, exp, pat_expr_list, ptial) :: k) 
+	   | _ -> simpl_expr senv e0 (Cmatch (senv, exp, pat_expr_list, ptial) :: k) 
+           end
       | _ -> simpl_expr senv e0 (Cmatch (senv, exp, pat_expr_list, ptial) :: k) 
       end
   | Texp_try (e, pat_expr_list) ->
      simpl_expr senv e ((Ctry pat_expr_list) :: k) 
   | Texp_tuple (es) -> 
      let new_es = List.map (fun e -> simpl_expr senv e []) es in
-     rebuild senv (mkexp (Texp_tuple new_es)) k
-  | Texp_construct (path, constr_desc, es) -> 
-     let new_es = List.map (fun e -> simpl_expr senv e []) es in
-     rebuild senv (mkexp (Texp_construct (path, constr_desc, new_es))) k
+     rebuild (mkexp (Texp_tuple new_es)) k
+  | Texp_construct (path, cdesc, es) -> 
+     begin match es with
+     | [] -> rebuild exp k
+     | (e::l) -> simpl_expr senv e (Ccons(senv, exp, path, cdesc, [], l) :: k)
+     end
   | Texp_ifthenelse (e0, e1, e2opt) -> 
-     (* if (if e0 then e1 else e2) then e11 else e22 
-        ==> [if-if]
-        if e0 then (if e1 then e11 else e22)
-              else (if e2 then e11 else e22)
-     *)
      begin match k with
      | (Cif (env, e11, e22opt) :: k1) -> 
+       (* [if-if] *)
 	 let rhs =  {e1 with exp_desc = Texp_ifthenelse (e0, 
 	   { e1 with exp_desc = Texp_ifthenelse (e1, e11, e22opt) },
            match e2opt with
@@ -353,32 +367,24 @@ let rec simpl_expr (senv : ThmEnv.t) (exp : expression) (k: cont list) : express
          let rhs = {e_match with exp_desc = Texp_let (rflag, pat_expr_list,
               {e_match with exp_desc = Texp_match (expr, alts, ptial)})}
          in simpl_expr env rhs k1
-     | (Cif (env, then_e, else_eopt):: k1) -> 
-       (* if (let x = e1 in e2) then .. else ..
-           ==> [if-let]
-          let x = e1 in if e2 then .. else ..
-       *)
-         let rhs = {then_e with exp_desc = Texp_let (rflag, pat_expr_list,
-              {then_e with exp_desc = Texp_ifthenelse (expr, then_e, else_eopt)})}
-         in simpl_expr env rhs k1     
      | _ -> begin match pat_expr_list with
        | [] -> simpl_expr senv expr k
        | (p,e)::l ->  begin match (p.pat_desc, e.exp_desc) with
 	       | (Tpat_var (id1), Texp_ident (Pident id2, _)) 
                   when rflag = Nonrecursive && id1 = id2 -> 
 		    simpl_expr senv ({exp with exp_desc = Texp_let (rflag, l, expr)}) k
-	       | _ -> simpl_expr senv e (Clet (rflag, [], p, l, expr) ::k)
+	       | _ -> simpl_expr senv e (Clet (senv, rflag, [], p, l, expr) ::k)
 		  end
            end
       end
   | Texp_sequence (e1, e2) -> 
      let new_e1 = simpl_expr senv e1 k in 
      let new_e2 = simpl_expr senv e2 k in 
-     rebuild senv (mkexp (Texp_sequence (new_e1, new_e2))) k
+     rebuild (mkexp (Texp_sequence (new_e1, new_e2))) k
   | Texp_array (es) -> 
      let new_es =  List.map (fun e -> simpl_expr senv e []) es in
-     rebuild senv (mkexp (Texp_array new_es)) k
-  | others -> rebuild senv exp k
+     rebuild (mkexp (Texp_array new_es)) k
+  | others -> rebuild exp k
 
 (* This is for dealing with primitive binary operators such as > , <, etc *)
 and simpl_primitive_app senv exp f args k = match args with
@@ -429,9 +435,9 @@ and simpl_primitive_app senv exp f args k = match args with
       simpl_expr senv ({exp with exp_desc = Texp_ifthenelse (e0, 
 	{exp with exp_desc = new_e1}, Some {exp with exp_desc = new_e2})}) k
     end
- | _ ->  rebuild senv exp k
+ | _ ->  rebuild exp k
    end
-| _ ->  rebuild senv exp k
+| _ ->  rebuild exp k
 
 and simpl_args senv f ds nds res_type k = match nds with
 | [] -> (* this means all args are simplified *)
@@ -450,7 +456,7 @@ and simpl_args senv f ds nds res_type k = match nds with
                           exp_env  = p.pat_env } in
           let env2     = extend_senv senv id eid in
           begin match ds with
-          | [] -> rebuild senv f k 
+          | [] -> rebuild f k 
           | [(None, optl)] -> 
 	      simpl_expr senv e k
           | [(Some a, optl)] -> 
@@ -474,12 +480,12 @@ and simpl_args senv f ds nds res_type k = match nds with
           | (None, optl)::rest -> 
 	      simpl_args senv e rest [] e.exp_type k
 	  end
-      | _ -> rebuild senv expr k
+      | _ -> rebuild expr k
       end 
     | Texp_ident(path, vd) -> 
 	begin match vd.val_kind with
 	| Val_prim _ -> simpl_primitive_app senv expr f ds k 
-	| _ -> rebuild senv expr k
+	| _ -> rebuild expr k
 	end
     | Texp_let(rflag, pat_exp_list, e2) -> 
 	(* (let x = e1 in \y.e') a ==> let x = e1 in (\y.e') a *)
@@ -493,7 +499,7 @@ and simpl_args senv f ds nds res_type k = match nds with
                       | Some else_e -> Some { expr with exp_desc = 
 					           Texp_apply(else_e, ds) } in
        simpl_expr senv ({expr with exp_desc = Texp_ifthenelse(e0, new_then, new_else)}) k
-    | _ -> rebuild senv expr k
+    | _ -> rebuild expr k
     end    
 | ((Some e, optl) :: l) -> 
     simpl_expr senv e (Cargs (senv, f, ds, optl, l, res_type) :: k)
@@ -502,8 +508,8 @@ and simpl_args senv f ds nds res_type k = match nds with
           
 and rebuildMatch senv scrut aval alts ptial k = 
    let env1 = extend_denv senv scrut aval in
-   let (_,e) = List.hd alts in
    let goal_tasks = goalTasks senv in 
+   let (_,e) = List.hd alts in
    let new_alts = List.map (fun (p,e) -> 
    let env2 = add_tasks env1 (bound_vars_to_logic p) in
    if is_bad e then
@@ -525,14 +531,14 @@ and rebuildMatch senv scrut aval alts ptial k =
    	   let senv2  = extend_senv env4 id1 eid in 
    	   let senv3  = extend_denv senv2 eid (Inline ({scrut with exp_desc = 
    					     Texp_construct(path,cdesc,[])})) in
-             (p, simpl_expr senv3 e k) 
-           | _ -> (p,simpl_expr env4 e k)
+             (p, simpl_expr senv3 e []) 
+           | _ -> (p,simpl_expr env4 e [])
      end 
      end 
     else let env4 = add_tasks env2 [toAxiom_peq scrut p] in
-         (p,simpl_expr env4 e k)
+         (p,simpl_expr env4 e [])
     ) alts in
-   {e with exp_desc = Texp_match (scrut, new_alts, ptial)}
+   rebuild {e with exp_desc = Texp_match (scrut, new_alts, ptial)} k
 
 and ergo_counter = ref 1
 
@@ -553,24 +559,25 @@ and rebuildIf senv scrut e1 e2opt k =
     match is_expression_true scrut with
      | Ptrue -> simpl_expr senv e1 k
      | Pfalse -> begin match e2opt with
-       | None -> rebuild senv (mkexp (Texp_ifthenelse (scrut, unr_exp, None))) k
+       | None -> rebuild (mkexp (Texp_ifthenelse (scrut, unr_exp, None))) k
        | Some e2 -> simpl_expr senv e2 k
        end 
      | Pothers -> begin match e2opt with
        | Some e2 -> begin match e2.exp_desc with
-	 | Texp_bad _ when (is_scrutinee_ergoble scrut) -> 
+	 | Texp_bad _ when (is_expression_ergoble scrut) -> 
              let goal_tasks = goalTasks senv in        
 	     let senv1 = if is_prop
                          then add_tasks senv (goal_tasks@[toGoal scrut])
 	                 else add_tasks senv (goal_tasks@[toGoal_beq scrut]) in
 	     let ts1   = tasks senv1 in     
              let inits = (Location.toString scrut.exp_loc) in
-	     let filename = inits^"_"^(string_of_int !ergo_counter)^"_if.why" in
+	     let filename = inits^"_"^(string_of_int !ergo_counter)^"_ifelse.why" in
              ergo_counter := !ergo_counter + 1;
 	     write_tasks_to_file filename ts1;
-	     (* print_string "call altergo: \n"; print_expression scrut; *)
+	     (* trace ("call altergo "^filename^": \n") print_expression scrut; *)
 	     begin match askErgo filename ts1 with 
 	     | Valid -> (* scrutinee is Valid *)
+		 (* print_string "Valid"; *)
 		 simpl_expr then_senv2 e1 k
 	     | _ -> (* we omit the negation check for the moment
 		       let senv2 = add_tasks senv (goal_tasks@[toGoal_bneg scrut]) in
@@ -583,22 +590,46 @@ and rebuildIf senv scrut e1 e2opt k =
                        let else_senv2 = add_tasks else_senv 
 		       [toAxiom_bneq scrut] in
                        simpl_expr else_senv2 e2 k
-		       | None -> rebuild senv (mkexp (Texp_ifthenelse 
+		       | None -> rebuild (mkexp (Texp_ifthenelse 
 		       ((falseExpression scrut), unr_exp, None))) k
 		       end 
 		       | _ -> *) (* no validity info about scrutinee *)
+		 (* print_string "Don't know"; *)
 		 let new_e1 = simpl_expr then_senv2 e1 [] in
-		 rebuild senv (mkexp (Texp_ifthenelse 
+		 rebuild (mkexp (Texp_ifthenelse 
 					   (scrut, new_e1, e2opt))) k
              end
 	 | _ -> 
+	     begin match e1.exp_desc with
+             | Texp_bad _  when (is_expression_ergoble scrut) -> 
+		  let goal_tasks = goalTasks senv in        
+	     let senv1 = if is_prop
+                         then add_tasks senv (goal_tasks@[toGoal_neg scrut])
+	                 else add_tasks senv (goal_tasks@[toGoal_bneq scrut]) in
+	     let ts1   = tasks senv1 in     
+             let inits = (Location.toString scrut.exp_loc) in
+	     let filename = inits^"_"^(string_of_int !ergo_counter)^"_ifthen.why" in
+             ergo_counter := !ergo_counter + 1;
+	     write_tasks_to_file filename ts1;
+	     (* trace ("call altergo "^filename^": \n") print_expression scrut; *)
+	     begin match askErgo filename ts1 with 
+	     | Valid -> (* scrutinee is Valid *)
+		 (* print_string "Valid"; *)
+		 simpl_expr else_senv2 e2 k
+	     | _ -> (* print_string "Don't know"; *)
+		 let new_e2 = simpl_expr else_senv2 e2 [] in
+		 rebuild (mkexp (Texp_ifthenelse 
+					   (scrut, e1, Some new_e2))) k
+             end
+	     | _ ->
 	     let new_e1 = simpl_expr then_senv2 e1 [] in
              let new_e2 = Some (simpl_expr else_senv2 e2 []) in
-	     rebuild senv (mkexp (Texp_ifthenelse (scrut, new_e1, new_e2))) k
+	     rebuild (mkexp (Texp_ifthenelse (scrut, new_e1, new_e2))) k
+            end
         end
        | None -> 	     
 	   let new_e1 = simpl_expr then_senv2 e1 [] in
-	   rebuild senv (mkexp (Texp_ifthenelse (scrut, new_e1, None))) k
+	   rebuild (mkexp (Texp_ifthenelse (scrut, new_e1, None))) k
        end
    
 (* 
@@ -617,6 +648,7 @@ and knownCon senv (path, cdesc) es alts k =
     let xs = List.filter (fun (p,e) -> match p.pat_desc with
     | Tpat_construct (path2, cdesc2, ps) -> cdesc.cstr_tag = cdesc2.cstr_tag
     | _ -> false) alts in
+    print_string "No branch is matched";
     let (p,e) = List.hd xs in
     match p.pat_desc with
     | Tpat_construct (path2, cdesc2, ps) -> 
@@ -625,47 +657,94 @@ and knownCon senv (path, cdesc) es alts k =
     | _ -> raise(Error(KnownCon_impossible_pattern))   
    
 
-and rebuild senv a k = 
+and rebuild a k = 
+  trace "***esc.rebuild" print_expression a;
   (* print_string "***esc.rebuild: \n"; print_expression a; print_string "\n"; *)
   match (a.exp_desc, k) with
   | (_, []) -> a
-  | (Texp_bad (bl), Cmatch _ :: k1) -> rebuild senv a k1
-  | (Texp_bad (bl), Cif _ :: k1) -> rebuild senv a k1
-  | (Texp_bad (bl), Capp _ :: k1) -> rebuild senv a k1
-  | (Texp_bad (bl), Cargs _ :: k1) -> rebuild senv a k1
-  | (Texp_bad (bl), Clet _ :: k1) -> rebuild senv a k1
-  | (Texp_bad (bl), Cin _ :: k1) -> rebuild senv a k1
-  | (Texp_unr (bl), Cmatch _ :: k1) -> rebuild senv a k1
-  | (Texp_unr (bl), Cif _ :: k1) -> rebuild senv a k1
-  | (Texp_unr (bl), Capp _ :: k1) -> rebuild senv a k1
-  | (Texp_unr (bl), Cargs _ :: k1) -> rebuild senv a k1
-  | (Texp_unr (bl), Clet _ :: k1) -> rebuild senv a k1
-  | (Texp_unr (bl), Cin _ :: k1) -> rebuild senv a k1
+  | (Texp_bad (bl), Cmatch _ :: k1) -> rebuild a k1
+  | (Texp_bad (bl), Cif _ :: k1) -> rebuild a k1
+  | (Texp_bad (bl), Capp _ :: k1) -> rebuild a k1
+  | (Texp_bad (bl), Cargs _ :: k1) -> rebuild a k1
+  | (Texp_bad (bl), Cprim _ :: k1) -> rebuild a k1
+  | (Texp_bad (bl), Ccons _ :: k1) -> rebuild a k1
+  | (Texp_bad (bl), Clet _ :: k1) -> rebuild a k1
+  | (Texp_bad (bl), Cin _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Cmatch _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Cif _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Capp _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Cargs _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Cprim _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Ccons _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Clet _ :: k1) -> rebuild a k1
+  | (Texp_unr (bl), Cin _ :: k1) -> rebuild a k1
   | (Texp_construct (path, cdesc, es), 
      Cmatch (matchenv, e_match, alts, ptial) :: k1) -> 
       knownCon matchenv (path, cdesc) es alts k1
   | (_, CLam (e, p, ptial) :: k1) -> 
-      rebuild senv {e with exp_desc = Texp_function ([(p,a)], ptial)} k1
+      rebuild {e with exp_desc = Texp_function ([(p,a)], ptial)} k1
   | (_, Cargs (env, f, ds, optl, nds, res_type) :: k1) -> 
       simpl_args env f (ds@[(Some a, optl)]) nds res_type k1
   | (_, Capp (env, ds, nds, res_type) :: k1) -> 
       simpl_args env a ds nds res_type k1
-  | (_, Clet (rflag, ds, p, uds, e3) :: k1) ->       
+  | (_, Ccons(env, e, path, cdesc, ds, uds) :: k1) -> 
+       begin match uds with
+       | [] -> if List.for_all is_expression_tvalue ds then
+	   begin match a.exp_desc with
+	   | Texp_match(e0, pat_exp_list, ptial) ->
+	       rebuildMatch env e0 NoVal
+		   (List.map (fun (pi,ei) -> (pi,
+                {ei with exp_desc=Texp_construct(path, cdesc, ds@[ei])}))
+			  pat_exp_list) ptial k1
+	   | Texp_ifthenelse(a0, a1, a2opt) -> 
+	     let new_a1 = {a1 with exp_desc=Texp_construct(path,cdesc,ds@[a1])} in
+             let new_a2opt = match a2opt with
+	   | None -> None
+	   | Some a2 -> Some ({a2 with exp_desc=Texp_construct(path,cdesc,ds@[a2])}) in
+	     rebuildIf env a0 new_a1 new_a2opt k1
+	   | Texp_let (rflag, pat_exp_list, expr) ->
+	       let e2 = {e with exp_desc=Texp_construct(path,cdesc,ds@[expr])} in
+	       rebuild ({expr with exp_desc=Texp_let(rflag, pat_exp_list, e2)}) k1
+	   | _ -> 
+	       rebuild ({e with exp_desc=Texp_construct(path,cdesc,ds@[a])}) k1
+           end
+            else rebuild ({e with exp_desc=Texp_construct(path,cdesc,ds@[a])}) k1
+       | (x::l) -> 
+	   if List.for_all is_expression_tvalue ds then
+         begin match x.exp_desc with
+	 | Texp_match(e0, pat_exp_list, ptial) -> 
+	     let alts = List.map (fun (pi,ei) -> (pi, 
+	    {ei with exp_desc=Texp_construct(path, cdesc, ds@[a;ei]@l)}))
+		 pat_exp_list in
+	     simpl_expr env x (Cmatch (env, x, alts, ptial) :: k1)
+	 | Texp_ifthenelse(e0, e1, e2opt) ->
+           let new_e1 = {e1 with exp_desc=Texp_construct(path,cdesc,ds@[a;e1]@l)} in
+           let new_e2opt = match e2opt with
+	   | None -> None
+	   | Some e2 -> Some ({e2 with exp_desc=Texp_construct(path,cdesc,ds@[a;e2]@l)}) in
+	     simpl_expr env e0 (Cif (env, new_e1, new_e2opt) :: k1)
+         | _ -> simpl_expr env x (Ccons(env,e,path,cdesc,ds@[a],l) :: k1)
+	 end
+       else rebuild ({e with exp_desc=Texp_construct(path,cdesc,ds@[a])}) k1    
+   end
+  | (_, Clet (senv, rflag, ds, p, uds, e3) :: k1) ->       
       begin match p.pat_desc with
-      | Tpat_var (id1) when rflag = Nonrecursive && 
-	  ((is_expression_tvalue a) || (match e3.exp_desc with
+      | Tpat_var (id1) when rflag = Nonrecursive &&
+  	  ((is_expression_tvalue a) || (match e3.exp_desc with
 	  | Texp_ident(Pident id2, vd) -> id2 = id1 
 	  | _ -> false)) ->
-        let new_id = Ident.rename id1 in 
-  	let vd     = { val_type = a.exp_type; val_kind = Val_reg } in
-	let eid    = {a with exp_desc = Texp_ident(Pident new_id, vd)} in
-	let env2   = extend_senv senv id1 eid in
-	let env3   = extend_denv env2 eid (Inline a) in  
+              let new_id = Ident.rename id1 in 
+	      let vd     = { val_type = a.exp_type; val_kind = Val_reg } in
+	      let eid    = {a with exp_desc = Texp_ident(Pident new_id, vd)} in
+	      let env2   = extend_senv senv id1 eid in
+	      let new_senv = extend_denv env2 eid (Inline a) in
+           (* else extend_denv senv {a with exp_desc=Texp_ident(Pident id1, vd)} (Inline a) *)
+        
 	  begin match uds with
-	  | [] -> simpl_expr env3 e3 (Cin (rflag, ds) :: k1)
+	  | [] -> simpl_expr new_senv e3 (Cin (rflag, ds) :: k1)
 	  | ((x,e)::l) ->
-	      simpl_expr env3 e (Clet (rflag, ds, x, l, e3) :: k1)	      
-	  end	  
+	      simpl_expr new_senv e (Clet (new_senv, rflag, ds, x, l, e3) :: k1)
+	  end	            
      | _ -> begin match a.exp_desc with
        | Texp_let(rec_flag, pelist, a2) -> 
 	   (* let x = (let y = a1 in a2) in e3 ==> [let-let]
@@ -677,7 +756,7 @@ and rebuild senv a k =
 	      simpl_expr env2 e3 (Cin (rflag, ds@pelist@[(p,a2)]) :: k1)
             | ((x,e)::l) ->
 	      let env2 = add_tasks senv ((bound_vars_to_logic p)@[toAxiom_peq a p]) in
-	      simpl_expr env2 e (Clet (rflag, ds@[(p,a2)], x, l, e3) :: k1)
+	      simpl_expr env2 e (Clet (env2, rflag, ds@[(p,a2)], x, l, e3) :: k1)
 	  end 
        | Texp_ifthenelse (a0, a1, a2opt) when rflag = Nonrecursive ->
 	 (* let x1 = ..
@@ -685,13 +764,15 @@ and rebuild senv a k =
                 xn = ..
             in e3  ==>  [let-if]
             let x1 = ..
-                if a0 then let x = a1 
+            in  if a0 then let x = a1 
 	                       xn = ..
                            in e3 
 	              else let x = a2 
 	                       xn = ..
                            in e3 *)
-           let e1 = {a1 with exp_desc = Texp_let (rflag, (p,a1)::uds, e3)} in
+           let e1 = match a1.exp_desc with
+ 	          | Texp_bad _ | Texp_unr _ -> a1
+	          | _ -> {a1 with exp_desc = Texp_let (rflag, (p,a1)::uds, e3)} in
 	   let e2opt = match a2opt with 
 	       | None -> None
 	       | Some a2 -> begin match a2.exp_desc with
@@ -700,28 +781,56 @@ and rebuild senv a k =
 			               Texp_let (rflag, (p,a2)::uds, e3)}
 	       end
 	   in rebuildIf senv a0 e1 e2opt (Cin (rflag, ds) :: k1)
+       | Texp_match(a0, pat_exp_list, ptial) when rflag = Nonrecursive ->
+	   (* let x1 = ..
+                x = match a0 with pi-> ei
+                xn = ..
+              in e3  ==>  [let-match]
+              let x1 = ..
+              in match a0 with pi -> let x = a1 
+	                                xn = ..
+                                    in e3 
+           *)
+	   let alts = List.map (fun (pi,ai) ->
+              (pi, match ai.exp_desc with
+	      | Texp_bad _ | Texp_unr _ -> ai
+	      | _ -> {ai with exp_desc = Texp_let (rflag, (p,ai)::uds, e3)}))
+	        pat_exp_list in
+	   rebuildMatch senv a0 NoVal alts ptial (Cin (rflag, ds) :: k1)
        | _ -> 	   
 	   let env2 = add_tasks senv ((bound_vars_to_logic p)@[toAxiom_peq a p]) in
 	   begin match uds with
 	   | [] ->  simpl_expr env2 e3 (Cin (rflag, ds@[(p,a)]) :: k1) 
 	   | ((x,e)::l) -> 
-	      simpl_expr env2 e (Clet (rflag, ds@[(p,a)], x, l, e3) :: k1)
+	      simpl_expr env2 e (Clet (env2, rflag, ds@[(p,a)], x, l, e3) :: k1)
            end
       end
     end
   | (_, Cin (rflag, ds) :: k1) -> 
       begin match ds with 
-      | [] -> rebuild senv a k1
-      | _ -> rebuild senv ({a with exp_desc = Texp_let (rflag, ds, a)}) k1
+      | [] -> rebuild a k1
+      | _ -> rebuild ({a with exp_desc = Texp_let (rflag, ds, a)}) k1
       end
   | (_, Cmatch (matchenv, e_match, alts, ptial) :: k1) -> 
+       let senv = matchenv in
        begin match lookup_denv a senv with
        | Inline e -> (* if scrutinee reappears, replace it by its aval *)
-                     rebuildMatch matchenv e NoVal alts ptial k1
+                     rebuildMatch senv e NoVal alts ptial k1
        | _ -> (* [[ a ]]_(K x) *)
+	 begin match a.exp_desc with
+	 | Texp_match (a0, pat_exp_list, ptial2) ->
+	     (* match (match a0 with pi -> ai) with alts 
+                ==> [match-match]
+                match a0 with pi -> match ai with alts 
+             *)
+	     let new_alts = List.map (fun (pi,ai) ->
+	       (pi, {e_match with exp_desc=Texp_match(ai,alts,ptial)}))
+		 pat_exp_list in
+	     rebuildMatch matchenv a0 NoVal new_alts ptial k1
+	 | _ -> 
          if a.exp_type = Predef.type_bool 
 	   then begin 
-             let goal_tasks = goalTasks senv in
+             let goal_tasks = goalTasks matchenv in
              let senv1  = begin if is_expression_prop a
 	                  then add_tasks senv (goal_tasks@[toGoal a])
                           else add_tasks senv (goal_tasks@[toGoal_beq a]) end in
@@ -742,34 +851,63 @@ and rebuild senv a k =
 	        rebuildMatch matchenv a NoVal alts ptial k1 end
             else rebuildMatch matchenv a NoVal alts ptial k1 
        end
-  | (_, Cif (ifenv, e1, e2opt) :: k1) ->       
-      begin match lookup_denv a senv with
+    end
+  | (_, Cif (env, e1, e2opt) :: k1) ->       
+      begin match lookup_denv a env with
       | Inline e -> (* if scrutinee reappears, replace it by its aval *)
-                    rebuildIf ifenv e e1 e2opt k1
+                    rebuildIf env e e1 e2opt k1
       | _ -> begin match a.exp_desc with
-        | Texp_let (rflag, pelist, e) -> 
+        | Texp_let (rflag, pelist, a2) -> 
        (* if (let x = a1 in a2) then .. else ..
            ==> [if-let]
           let x = a1 in if a2 then .. else ..
        *)
-	  rebuild senv e (Cif (ifenv, e1, e2opt):: Cin (rflag, pelist) :: k1)     
-        | _ -> rebuildIf ifenv a e1 e2opt k1
+	  rebuildIf env a2 e1 e2opt (Cin (rflag, pelist) :: k1)     
+	| Texp_ifthenelse (a0, a1, a2opt) -> 
+	    (* if (if a0 then a1 else a2) then e1 else e2 
+              ==> [if-if]
+            if a0 then (if a1 then e1 else e2)
+            else (if a2 then e1 else e2)
+		*)
+	  let new_e1 = {e1 with exp_desc = Texp_ifthenelse(a1,e1,e2opt)} in
+          let new_e2opt = match a2opt with
+	   | None -> None
+           | Some a2 -> Some ({e1 with exp_desc = Texp_ifthenelse(a2,e1,e2opt)})
+	  in rebuildIf env a0 new_e1 new_e2opt k1
+	| Texp_match(a0, pat_exp_list, ptial) ->
+	   (* if (match a0 with pi -> ai) then e1 else e2
+             ==> [if-match]
+              match a0 with pi -> if ai then e1 else e2
+	   *)
+	  let alts = List.map (fun (pi,ai) ->
+               (pi, {e1 with exp_desc = Texp_ifthenelse(ai,e1,e2opt)})) pat_exp_list in
+	  rebuildMatch env a0 NoVal alts ptial k1
+        | _ -> rebuildIf env a e1 e2opt k1
         end
       end
+  | (_, Cthen (env, a0, e2opt) :: k1) -> 
+      begin match e2opt with
+      | None ->       
+          rebuild ({a with exp_desc = Texp_ifthenelse(a0,a,None)}) k1
+      | Some e2 -> 
+          simpl_expr env e2 (Celse (a0, a) :: k1)
+      end
+  | (_, Celse (a0, a1) :: k1) -> 
+      rebuild ({a1 with exp_desc = Texp_ifthenelse(a0,a1,Some a)}) k1
   | _ -> raise(Error(Rebuild_pattern_not_matched))
   
 
-and rebuildVar senv ((n, e):(Ident.t * expression)) 
+and rebuildVar ((n, e):(Ident.t * expression)) 
                (v:aval) (k:cont list) : outexp = 
 (* e is the expression form of the ident n *)
     match v with
-    | Inline a -> rebuild senv a k
+    | Inline a -> rebuild a k
     | NotCon (cs) -> begin match k with
       | Cmatch (senv, e_match, alts, ptial) :: k1 -> 
 	  rebuildMatch senv e (NotCon cs) alts ptial k1
-      | _ -> rebuild senv e k
+      | _ -> rebuild e k
       end
-    | _ -> rebuild senv e k
+    | _ -> rebuild e k
 
 (* report static contract checking error message *)
 
@@ -848,6 +986,7 @@ let static_report (id, exp) validity =
 
 let rec has_function_call gamma exp = match exp.exp_desc with
 | Texp_ident (path, vd) -> if Tbl.mem path gamma then true else false
+| Texp_constant _ -> false
 | Texp_bad (bl) -> false
 | Texp_unr (bl) -> false
 | Texp_let (rec_flag, pat_expr_list, expr1) -> 
@@ -863,6 +1002,7 @@ let rec has_function_call gamma exp = match exp.exp_desc with
        has_function_call (add_fnames pat_expr_list gamma) expr1
 | Texp_function (pat_expr_list, partial) -> 
   List.exists (fun (p,e) -> has_function_call gamma e) pat_expr_list
+| Texp_apply (e1, _) -> has_function_call gamma e1
 | Texp_match (expr1, pat_expr_list, partial) ->
   if has_function_call gamma expr1 then true
   else List.exists (fun (p,e) -> has_function_call gamma e) pat_expr_list
@@ -938,36 +1078,50 @@ let rec rmUNR exp =
   | _ -> expr
   in map_expression removeUNR exp
 
-let static_contract_checking env contract_flag (id, exp) = 
+let inline_rec id exp exp1 = 
+  let expand_id e = match e.exp_desc with
+  | Texp_ident(path, vd) ->
+     if Path.unique_name path = Ident.unique_name id
+       then begin 
+	    rename_boundvars Tbl.empty exp1
+	    end
+       else e
+  | _ -> e
+  in  map_expression expand_id exp
+
+let rec static_contract_checking env contract_flag (id, exp) = 
   try
-  (* print_string "\n raw expression: \n"; print_expression exp; *)
-  let sexp =  simpl_expr (update_name env (Pident id)) exp [] in
-  (* print_string "\n simplified expression: \n"; print_expression sexp; *)
+  trace "raw expression" print_expression exp; 
+  let senv = update_name env (Pident id) in
+  let sexp =  simpl_expr senv exp [] in
+  trace "simplified expression" print_expression sexp; 
   let cleaned_sexp = rmUNR sexp in
-  (* print_string "\n**residual code: \n"; print_expression cleaned_sexp; *)
+  (* trace "***residual code" print_expression cleaned_sexp; *)
   let (counter_example, has_bad) = check cleaned_sexp in
-  let validity = 
-      if has_bad 
-      then begin 
-           if contract_flag = -1 
-           then begin print_string ("\n**residual code of "^(Ident.name id)^": \n"); 
- 	        print_expression sexp; 
-                EscSyn.Unknown
-                end
-           else EscSyn.Unknown
+  if has_bad 
+      then begin
+	   let validity = EscSyn.Unknown in
+	   let rpt = static_report (id, counter_example) validity in 
+            print_string ("At depth "^string_of_int(depth env)^", ");
+            fprintf std_formatter "%s" rpt; 
+	   match ThmEnv.depth env with
+	   | 0 -> 
+	    let new_senv = increase_depth env in  
+            static_contract_checking new_senv contract_flag (id,sexp)
+	   | 1 ->  
+	    let the_exp = lookup_rec_env id env in
+            let expanded_exp = inline_rec id sexp the_exp in
+	    let new_senv = increase_depth env in  
+            static_contract_checking new_senv contract_flag (id,expanded_exp)
+           | _ -> 
+               (cleaned_sexp, validity)
            end
-      else EscSyn.Valid
-                 (*  if has_function_call 
-                           function_names counter_example 
-                      then Unknown
-                      else Invalid  *)
-  in 
-  (* print_string "\n validity: "; print_validity validity; *)
-  (* write_tasks_to_file ((Ident.name id)^".why") (tasks env); *)
-  print_newline ();
-  let rpt = static_report (id, counter_example) validity in
-  fprintf std_formatter "%s" rpt;
-  (cleaned_sexp, validity)
+      else
+       let validity =  EscSyn.Valid in
+       let rpt = static_report (id, counter_example) validity in
+       print_string ("At depth "^string_of_int(depth env)^", ");
+       fprintf std_formatter "%s" rpt; 
+       (cleaned_sexp, validity)
   with Error(err) -> report_error std_formatter err;
                      raise (Error(err))
 
diff --git a/verify/escSyn.ml b/verify/escSyn.ml
index c94f85eb27..e287d3e36b 100644
--- a/verify/escSyn.ml
+++ b/verify/escSyn.ml
@@ -1,6 +1,14 @@
 open Types
 open Typedtree
 open Path
+open Format
+
+let should_trace = false
+(* try ignore(Sys.getenv "-trace"); true
+   with Not_found -> false *)
+
+let trace msg fn arg = if should_trace 
+  then (printf "%s:\n" msg; fn arg; print_newline())
 
 type validity = Valid | Invalid | Unknown | HighFailure | Timeout
 
@@ -61,17 +69,324 @@ let rec is_expression_argable exp = match exp.exp_desc with
     List.for_all (fun (eopt, _) -> match eopt with
     | Some a -> is_expression_argable a
     | None -> false) args
+| Texp_construct (path, cdesc, es) -> 
+    List.for_all is_expression_argable es
 | _ -> false
 
-let rec exn_to_bad exp = 
+let exn_to_bad exp = 
   let new_desc = match exp.exp_desc with
-  | Texp_ident (path, value_desc) -> 
+  (* | Texp_ident (path, value_desc) -> 
+      if (Path.name path) = "Pervasives.failwith"
+      then Texp_bad (Callee (exp.exp_loc, path))
+      else exp.exp_desc *)
+  | Texp_apply(e1,args) -> begin match e1.exp_desc with
+    | Texp_ident(path, value_desc) -> 
       if (Path.name path) = "Pervasives.failwith"
       then Texp_bad (Callee (exp.exp_loc, path))
       else exp.exp_desc
+    | _ -> exp.exp_desc
+    end
   | others -> others
   in {exp with exp_desc = new_desc}
 
 let pre_processing exp =  map_expression exn_to_bad exp
 
   
+let rec rename_path_ident boundvars path gamma = match path with
+ | Pident id -> if not(List.mem id boundvars) 
+                then try Pident (Tbl.find id gamma)
+		     with Not_found -> path
+                else path
+ | Pdot (p, s, pos) -> Pdot (rename_path_ident boundvars p gamma, s, pos)
+ | Papply (p1, p2) -> Papply(p1, rename_path_ident boundvars p2 gamma)
+
+(* subst replace free variables id1 in expr by id2 *)
+let rec subst bound_vars gamma expr = match expr.exp_desc with
+ | Texp_ident (path, vd) -> 
+     {expr with exp_desc = Texp_ident (rename_path_ident bound_vars path gamma, vd)}
+ | Texp_constant (c) -> expr
+ | Texp_let (rec_flag, pat_expr_list, e2) -> 
+     let bvars     = let_bound_idents pat_expr_list in
+     let p_e_list  = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) gamma e)) 
+	                   pat_expr_list in
+     let new_e2 = subst bound_vars gamma e2 in
+     {expr with exp_desc = Texp_let (rec_flag, p_e_list, new_e2)}
+ | Texp_function (pat_expr_list, ptial) -> 
+     let bvars     = let_bound_idents pat_expr_list in
+     let p_e_list  = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) gamma e)) 
+	                   pat_expr_list in
+     {expr with exp_desc = Texp_function (p_e_list, ptial)}
+ | Texp_apply (e1, es) ->
+     let new_e1 = subst bound_vars gamma e1 in
+     let new_es = List.map (fun (e_opt, optl) -> match e_opt with
+                            | Some e -> (Some (subst bound_vars gamma e), optl)
+                            | None -> (None, optl)) es
+     in {expr with exp_desc = Texp_apply (new_e1, new_es)}
+ | Texp_match (e0, pat_expr_list, ptial) -> 
+     let new_e0   = subst bound_vars gamma e0 in
+     let bvars    = let_bound_idents pat_expr_list in
+     let p_e_list = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) gamma e)) 
+ 	                     pat_expr_list in
+     {expr with exp_desc = Texp_match (new_e0, p_e_list, ptial)} 
+ | Texp_try (e1, pat_expr_list) -> 
+     let new_e1   = subst bound_vars gamma e1 in
+     let bvars    = let_bound_idents pat_expr_list in
+     let p_e_list = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) gamma e)) 
+ 	                     pat_expr_list in
+     {expr with exp_desc = Texp_try (new_e1, p_e_list)}
+ | Texp_tuple (es) -> 
+     let new_es = List.map (subst bound_vars gamma) es in
+     {expr with exp_desc = Texp_tuple new_es}
+ | Texp_construct (path, cdesc, es) -> 
+     let new_es = List.map (subst bound_vars gamma) es in
+     {expr with exp_desc = Texp_construct (path, cdesc, new_es)}
+ | Texp_variant (lbl, e_opt) -> 
+     let new_e = match e_opt with
+     | Some e -> Some (subst bound_vars gamma e)
+     | None -> None
+     in {expr with exp_desc = Texp_variant (lbl, new_e)}
+ | Texp_record (ldesc_expr_list, e_opt) ->
+     let l_e_list = List.map (fun (p,e) -> (p, subst bound_vars gamma e)) 
+ 	                     ldesc_expr_list in
+     {expr with exp_desc = Texp_record (l_e_list, match e_opt with
+     | Some e -> Some (subst bound_vars gamma e)
+     | None -> None)}
+ | Texp_field (e, ldesc) -> 
+     let new_e = subst bound_vars gamma e in
+     {expr with exp_desc = Texp_field (new_e, ldesc)}
+ | Texp_setfield (e1, ldesc, e2) -> 
+     let new_e1 = subst bound_vars gamma e1 in
+     let new_e2 = subst bound_vars gamma e2 in
+     {expr with exp_desc = Texp_setfield (new_e1, ldesc, new_e2)}
+ | Texp_array (es) -> 
+     let new_es = List.map (subst bound_vars gamma) es in
+     {expr with exp_desc = Texp_tuple new_es}
+ | Texp_ifthenelse (e0, e1, e2_opt) -> 
+     let new_e0 = subst bound_vars gamma e0 in
+     let new_e1 = subst bound_vars gamma e1 in
+     let new_e2 = match e2_opt with
+     | Some e -> Some (subst bound_vars gamma e)
+     | None -> None 
+     in {expr with exp_desc = Texp_ifthenelse (new_e0, new_e1, new_e2)}    
+ | Texp_sequence (e1, e2) -> 
+     let new_e1 = subst bound_vars gamma e1 in
+     let new_e2 = subst bound_vars gamma e2 in
+     {expr with exp_desc = Texp_sequence (new_e1, new_e2)}    
+ | Texp_while (e1, e2) -> 
+     let new_e1 = subst bound_vars gamma e1 in
+     let new_e2 = subst bound_vars gamma e2 in
+     {expr with exp_desc = Texp_while (new_e1, new_e2)}    
+ | Texp_for (id, e1, e2, dflag, e3) ->
+     let new_e1 = subst bound_vars gamma e1 in
+     let new_e2 = subst bound_vars gamma e2 in
+     let new_e3 = subst bound_vars gamma e3 in
+     {expr with exp_desc = Texp_for (id, new_e1, new_e2, dflag, new_e3)}    
+  | Texp_when (e1, e2) -> 
+     let new_e1 = subst bound_vars gamma e1 in
+     let new_e2 = subst bound_vars gamma e2 in
+     {expr with exp_desc = Texp_when (new_e1, new_e2)}    
+  | Texp_send (e, meth) -> 
+     let new_e = subst bound_vars gamma e in
+     {expr with exp_desc = Texp_send (new_e, meth)}    
+  | Texp_new _ -> expr
+  | Texp_instvar _ -> expr
+  | Texp_setinstvar (path1, path2, e) -> 
+     let new_e = subst bound_vars gamma e in
+     {expr with exp_desc = Texp_setinstvar(path1, path2, new_e)}
+  | Texp_override (path1, path_expr_list) -> 
+     let p_e_list = List.map (fun (p,e) -> (p, subst bound_vars gamma e)) 
+ 	                      path_expr_list in
+     {expr with exp_desc = Texp_override (path1, p_e_list)}
+  | Texp_letmodule (id, modexpr, e) -> 
+      let new_e = subst bound_vars gamma e in
+      {expr with exp_desc = Texp_letmodule (id, modexpr, new_e)}
+  | Texp_assert (e) -> 
+      let new_e = subst bound_vars gamma e in
+      {expr with exp_desc = Texp_assert(new_e)}
+  | Texp_assertfalse -> expr
+  | Texp_lazy (e) -> 
+      let new_e = subst bound_vars gamma e in
+      {expr with exp_desc = Texp_assert(new_e)}
+  | Texp_object _ -> expr
+  | Texp_pack _ -> expr
+  | Texp_local_contract (c, e) -> 
+      let new_e = subst bound_vars gamma e in
+      {expr with exp_desc = Texp_local_contract(c, new_e)}
+  | Texp_contract (c, e1, e2, e3) -> 
+      let new_e1 = subst bound_vars gamma e1 in
+      let new_e2 = subst bound_vars gamma e2 in
+      let new_e3 = subst bound_vars gamma e3 in
+      {expr with exp_desc = Texp_contract (c, new_e1, new_e2, new_e3)}    
+  | Texp_bad _ -> expr
+  | Texp_unr _ -> expr
+  | Texp_Lambda (ids, e) -> 
+      let new_e = subst bound_vars gamma e in
+      {expr with exp_desc = Texp_Lambda (ids, new_e)}
+  | Texp_App (e1, es) -> 
+      let new_e1 = subst bound_vars gamma e1 in
+      let new_es = List.map (subst bound_vars gamma) es in
+      {expr with exp_desc = Texp_App(new_e1, new_es)}
+  | Texp_raise (e) -> expr
+
+let rec rename_pattern gamma pat = match pat.pat_desc with
+| Tpat_var(id) -> 
+     {pat with pat_desc = try Tpat_var (Tbl.find id gamma)
+                 with Not_found -> Tpat_var(id)}
+   
+| d -> {pat with pat_desc = map_pattern_desc (rename_pattern gamma) d}
+
+let rec rename_boundvars gamma expr = match expr.exp_desc with
+ | Texp_ident (path, vd) ->
+     let new_id = rename_path_ident [] path gamma in
+     {expr with exp_desc = Texp_ident (new_id, vd)}
+ | Texp_constant (c) -> expr
+ | Texp_let (rec_flag, pat_expr_list, e2) -> 
+     let p_e_list  = List.map (fun (p,e) -> (p, rename_boundvars gamma e)) 
+	                   pat_expr_list in
+     let new_e2 = rename_boundvars gamma e2 in
+     {expr with exp_desc = Texp_let (rec_flag, p_e_list, new_e2)}
+ | Texp_function (pat_expr_list, ptial) ->      
+     let p_e_list  = List.map (fun (p,e) -> 
+       match p.pat_desc with
+       | Tpat_var(id) -> 
+	   let new_id = Ident.rename id in
+	   let new_gamma = Tbl.add id new_id gamma in
+	   ({p with pat_desc = Tpat_var(new_id)}, rename_boundvars new_gamma e)
+       | Tpat_construct(path, cdesc, ps) -> 
+	  let bvars = let_bound_idents pat_expr_list in
+	  let new_gamma = List.fold_right (fun i default -> 
+		    Tbl.add i (Ident.rename i) default) bvars gamma in
+	  let new_ps = List.map (rename_pattern new_gamma) ps in
+          ({p with pat_desc = Tpat_construct(path, cdesc, new_ps)},
+            rename_boundvars new_gamma e)
+       | _ -> (p, e))
+	                   pat_expr_list in
+     {expr with exp_desc = Texp_function (p_e_list, ptial)}
+ | Texp_apply (e1, es) ->
+     let new_e1 = rename_boundvars gamma e1 in
+     let new_es = List.map (fun (e_opt, optl) -> match e_opt with
+                            | Some e -> (Some (rename_boundvars gamma e), optl)
+                            | None -> (None, optl)) es
+     in {expr with exp_desc = Texp_apply (new_e1, new_es)}
+ | Texp_match (e0, pat_expr_list, ptial) -> 
+     let new_e0   = rename_boundvars gamma e0 in
+     let p_e_list = List.map (fun (p,e) -> 
+       match p.pat_desc with
+       | Tpat_var(id) -> 
+	   let new_id = Ident.rename id in
+	   let new_gamma = Tbl.add id new_id gamma in
+	   ({p with pat_desc = Tpat_var(new_id)}, rename_boundvars new_gamma e)
+       | Tpat_construct(path, cdesc, ps) -> 
+	  let bvars = List.fold_right (fun pi default -> 
+	                       default@(pat_bound_idents pi)) ps [] in
+	  let newbvars = List.map Ident.rename bvars in
+          let blist = List.combine bvars newbvars in
+	  let new_gamma = List.fold_right (fun (i,ni) default ->
+	                   Tbl.add i ni default) blist gamma in
+	  let new_ps = List.map (rename_pattern new_gamma) ps in
+          ({p with pat_desc = Tpat_construct(path, cdesc, new_ps)},
+            rename_boundvars new_gamma e)
+       | _ -> (p,e))
+ 	                     pat_expr_list in
+     {expr with exp_desc = Texp_match (new_e0, p_e_list, ptial)} 
+ | Texp_try (e1, pat_expr_list) -> 
+     let new_e1   = rename_boundvars gamma e1 in
+     let p_e_list = List.map (fun (p,e) -> (p, rename_boundvars gamma e)) 
+ 	                     pat_expr_list in
+     {expr with exp_desc = Texp_try (new_e1, p_e_list)}
+ | Texp_tuple (es) -> 
+     let new_es = List.map (rename_boundvars gamma) es in
+     {expr with exp_desc = Texp_tuple new_es}
+ | Texp_construct (path, cdesc, es) -> 
+     let new_es = List.map (rename_boundvars gamma) es in
+     {expr with exp_desc = Texp_construct (path, cdesc, new_es)}
+ | Texp_variant (lbl, e_opt) -> 
+     let new_e = match e_opt with
+     | Some e -> Some (rename_boundvars gamma e)
+     | None -> None
+     in {expr with exp_desc = Texp_variant (lbl, new_e)}
+ | Texp_record (ldesc_expr_list, e_opt) ->
+     let l_e_list = List.map (fun (p,e) -> (p, rename_boundvars gamma e)) 
+ 	                     ldesc_expr_list in
+     {expr with exp_desc = Texp_record (l_e_list, match e_opt with
+     | Some e -> Some (rename_boundvars gamma e)
+     | None -> None)}
+ | Texp_field (e, ldesc) -> 
+     let new_e = rename_boundvars gamma e in
+     {expr with exp_desc = Texp_field (new_e, ldesc)}
+ | Texp_setfield (e1, ldesc, e2) -> 
+     let new_e1 = rename_boundvars gamma e1 in
+     let new_e2 = rename_boundvars gamma e2 in
+     {expr with exp_desc = Texp_setfield (new_e1, ldesc, new_e2)}
+ | Texp_array (es) -> 
+     let new_es = List.map (rename_boundvars gamma) es in
+     {expr with exp_desc = Texp_tuple new_es}
+ | Texp_ifthenelse (e0, e1, e2_opt) -> 
+     let new_e0 = rename_boundvars gamma e0 in
+     let new_e1 = rename_boundvars gamma e1 in
+     let new_e2 = match e2_opt with
+     | Some e -> Some (rename_boundvars gamma e)
+     | None -> None 
+     in {expr with exp_desc = Texp_ifthenelse (new_e0, new_e1, new_e2)}    
+ | Texp_sequence (e1, e2) -> 
+     let new_e1 = rename_boundvars gamma e1 in
+     let new_e2 = rename_boundvars gamma e2 in
+     {expr with exp_desc = Texp_sequence (new_e1, new_e2)}    
+ | Texp_while (e1, e2) -> 
+     let new_e1 = rename_boundvars gamma e1 in
+     let new_e2 = rename_boundvars gamma e2 in
+     {expr with exp_desc = Texp_while (new_e1, new_e2)}    
+ | Texp_for (id, e1, e2, dflag, e3) ->
+     let new_e1 = rename_boundvars gamma e1 in
+     let new_e2 = rename_boundvars gamma e2 in
+     let new_e3 = rename_boundvars gamma e3 in
+     {expr with exp_desc = Texp_for (id, new_e1, new_e2, dflag, new_e3)}    
+  | Texp_when (e1, e2) -> 
+     let new_e1 = rename_boundvars gamma e1 in
+     let new_e2 = rename_boundvars gamma e2 in
+     {expr with exp_desc = Texp_when (new_e1, new_e2)}    
+  | Texp_send (e, meth) -> 
+     let new_e = rename_boundvars gamma e in
+     {expr with exp_desc = Texp_send (new_e, meth)}    
+  | Texp_new _ -> expr
+  | Texp_instvar _ -> expr
+  | Texp_setinstvar (path1, path2, e) -> 
+     let new_e = rename_boundvars gamma e in
+     {expr with exp_desc = Texp_setinstvar(path1, path2, new_e)}
+  | Texp_override (path1, path_expr_list) -> 
+     let p_e_list = List.map (fun (p,e) -> (p, rename_boundvars gamma e)) 
+ 	                      path_expr_list in
+     {expr with exp_desc = Texp_override (path1, p_e_list)}
+  | Texp_letmodule (id, modexpr, e) -> 
+      let new_e = rename_boundvars gamma e in
+      {expr with exp_desc = Texp_letmodule (id, modexpr, new_e)}
+  | Texp_assert (e) -> 
+      let new_e = rename_boundvars gamma e in
+      {expr with exp_desc = Texp_assert(new_e)}
+  | Texp_assertfalse -> expr
+  | Texp_lazy (e) -> 
+      let new_e = rename_boundvars gamma e in
+      {expr with exp_desc = Texp_assert(new_e)}
+  | Texp_object _ -> expr
+  | Texp_pack _ -> expr
+  | Texp_local_contract (c, e) -> 
+      let new_e = rename_boundvars gamma e in
+      {expr with exp_desc = Texp_local_contract(c, new_e)}
+  | Texp_contract (c, e1, e2, e3) -> 
+      let new_e1 = rename_boundvars gamma e1 in
+      let new_e2 = rename_boundvars gamma e2 in
+      let new_e3 = rename_boundvars gamma e3 in
+      {expr with exp_desc = Texp_contract (c, new_e1, new_e2, new_e3)}    
+  | Texp_bad _ -> expr
+  | Texp_unr _ -> expr
+  | Texp_Lambda (ids, e) -> 
+      let new_e = rename_boundvars gamma e in
+      {expr with exp_desc = Texp_Lambda (ids, new_e)}
+  | Texp_App (e1, es) -> 
+      let new_e1 = rename_boundvars gamma e1 in
+      let new_es = List.map (rename_boundvars gamma) es in
+      {expr with exp_desc = Texp_App(new_e1, new_es)}
+  | Texp_raise (e) -> expr
+
+
+       
diff --git a/verify/escSyn.mli b/verify/escSyn.mli
index 2fda43f453..eed401773f 100644
--- a/verify/escSyn.mli
+++ b/verify/escSyn.mli
@@ -6,6 +6,7 @@ type validity = Valid | Invalid | Unknown | HighFailure | Timeout
 
 type bool_info = Ptrue | Pfalse | Pothers
 
+val trace : string -> ('a -> unit) -> 'a -> unit
 val getop : Path.t -> string
 val is_pattern_true : pattern -> bool_info
 val is_expression_true : expression -> bool_info
@@ -13,3 +14,5 @@ val is_expression_bool : expression -> bool
 val is_expression_prop : expression -> bool
 val is_expression_argable : expression -> bool
 val pre_processing : expression -> expression
+val subst : Ident.t list -> (Ident.t, Ident.t) Tbl.t -> expression -> expression
+val rename_boundvars : (Ident.t, Ident.t) Tbl.t -> expression -> expression
diff --git a/verify/thmEnv.ml b/verify/thmEnv.ml
index 3900d4925d..bfe56016e6 100644
--- a/verify/thmEnv.ml
+++ b/verify/thmEnv.ml
@@ -49,28 +49,29 @@ type t = {
   opened_contract_decls: (Path.t * Types.contract_declaration) Ident.tbl; 
   axioms: axiom_declaration list;
   goalTasks: decl list;
-  abinds: (Ident.t, expression) Tbl.t;
-  vals: (expression, aval) Tbl.t;         (* variable |-> value *)
+  abinds: (Ident.t, expression) Tbl.t;    (* variable |-> tvalue *)
+  vals: (expression, aval) Tbl.t;         (* variable |-> expression *)
+  nonrecs : (Ident.t, expression) Tbl.t;  (* top-level nonrecursive functions *)
+  recs : (Ident.t, expression) Tbl.t;     (* top-level recursive functions *)
 }
 
+
 let init_tasks = 
-  let a_list = PPTexternal ([PPTvarid ("'a", Location.none)], "list", 
-                           Location.none) in
-  let a_b_arrow = PPTexternal ([PPTvarid ("'a", Location.none);
-                                PPTvarid ("'b", Location.none)], "arrow", 
-                              Location.none) in
-  let a_b_tuple = PPTexternal ([PPTvarid ("'a", Location.none);
-                                PPTvarid ("'b", Location.none)], "tuple", 
-                              Location.none) in
-  [TypeDecl (Location.none, ["'a";"'b"], "arrow");
-   TypeDecl (Location.none, ["'a";"'b"], "tuple");
-   Logic (Location.none, false, ["apply"], 
-          PFunction ([a_b_arrow; PPTvarid ("'a", Location.none)],
-          PPTvarid ("'b", Location.none)));
-   TypeDecl (Location.none, ["'a"], "list");
-   Logic (Location.none, false, ["nil"], PFunction ([], a_list));
-   Logic (Location.none, false, ["cons"], PFunction ([PPTvarid ("'a", Location.none); a_list], a_list ));
-   Logic (Location.none, false, ["tup"], PFunction ([PPTvarid ("'a", Location.none);PPTvarid ("'b", Location.none);], a_b_tuple));
+  let loc = Location.none in
+  let mklexpr desc = {pp_loc = loc; pp_desc = desc} in
+  let a = PPTvarid ("'a", loc) in
+  let b = PPTvarid ("'b", loc) in
+  let a_list = PPTexternal ([a], "list", loc) in
+  let a_b_arrow = PPTexternal ([a;b], "arrow", loc) in
+  let a_b_tuple = PPTexternal ([a;b], "tuple", loc) in
+  [TypeDecl (loc, ["'a";"'b"], "arrow");
+   TypeDecl (loc, ["'a";"'b"], "tuple");
+   Logic (loc, false, ["apply"], PFunction ([a_b_arrow; a], b));
+   TypeDecl (loc, ["'a"], "list");
+   Logic (loc, false, ["nil"], PFunction ([], a_list));
+   Logic (loc, false, ["cons"], PFunction ([a; a_list], a_list ));
+   Logic (loc, false, ["tup"], PFunction ([a;b], a_b_tuple));
+   Axiom (loc, "list_a0", mklexpr (PPforall(["x"], a, [], mklexpr(PPforall(["l"], a_list, [], mklexpr (PPinfix(mklexpr(PPvar "nil"), PPneq, mklexpr(PPapp("cons", [mklexpr(PPvar "x");mklexpr(PPvar "l")])))))))))
  ]
 
 (* empty environment *)
@@ -86,18 +87,26 @@ let initEnv l1 l2 = {
   goalTasks = []; (* represent a goal in terms of tasks *)
   abinds =  Tbl.empty;
   vals = Tbl.empty;
+  nonrecs = Tbl.empty;
+  recs = Tbl.empty;
 }
 
 (* Insertion of bindings by identifier *)
 
 let extend_senv env id1 id2 = {env with abinds = Tbl.add id1 id2 env.abinds}
 let extend_denv env exp aval = {env with vals = Tbl.add exp aval env.vals}
+let extend_nonrec_env env id1 e = {env with nonrecs = Tbl.add id1 e env.nonrecs}
+let extend_rec_env env id1 e = {env with recs = Tbl.add id1 e env.recs}
+
 
 (* the name of the current function under contract checking *)
 let update_name env n =  { env with name = n }
 
 let update_contract_name env n =  { env with contract_name = n }
 
+let decrease_depth env = { env with depth = env.depth - 1 }
+let increase_depth env = { env with depth = env.depth + 1 }
+
 let add_dep_contracts env x c = 
   { env with dep_contracts = Ident.add x c env.dep_contracts }
 
@@ -133,6 +142,10 @@ let lookup_senv id env = try let x = Tbl.find id env.abinds in
 let lookup_denv exp env = try Tbl.find exp env.vals
                           with Not_found -> NoVal
 
+let lookup_nonrec_env id env = Tbl.find id env.nonrecs
+let lookup_rec_env id env = Tbl.find id env.recs
+let recs env = env.recs
+let nonrecs env = env.nonrecs
 
 (* Error report *)
 
diff --git a/verify/thmEnv.mli b/verify/thmEnv.mli
index 52f396c36a..a01b6d5738 100644
--- a/verify/thmEnv.mli
+++ b/verify/thmEnv.mli
@@ -20,6 +20,8 @@ type t = {
   goalTasks: decl list;
   abinds: (Ident.t, expression) Tbl.t;
   vals: (expression, aval) Tbl.t;
+  nonrecs: (Ident.t, expression) Tbl.t;
+  recs: (Ident.t, expression) Tbl.t
 }
 
 val initEnv : contract_declaration list ->  
@@ -35,11 +37,19 @@ val goalTasks : t -> decl list
 val add_tasks : t -> decl list-> t
 val update_name : t -> Path.t -> t
 val update_contract_name : t -> Path.t -> t
+val decrease_depth : t -> t
+val increase_depth : t -> t
 val add_dep_contracts : t -> Ident.t -> Typedtree.core_contract -> t
 val add_contract_decl : t -> contract_declaration -> t
 val add_axiom : t -> axiom_declaration -> t
 val add_goalTasks : t -> decl list -> t
 val extend_senv : t -> Ident.t -> expression -> t
 val extend_denv : t -> expression -> aval -> t 
+val extend_nonrec_env : t -> Ident.t -> expression -> t
+val extend_rec_env : t -> Ident.t -> expression -> t
 val lookup_senv : Ident.t -> t -> aval
 val lookup_denv : expression -> t -> aval
+val lookup_nonrec_env : Ident.t -> t -> expression
+val lookup_rec_env : Ident.t -> t -> expression
+val nonrecs : t -> (Ident.t, expression) Tbl.t
+val recs : t -> (Ident.t, expression) Tbl.t
diff --git a/verify/thmProvers.ml b/verify/thmProvers.ml
index 4802cf689c..c5bec554dc 100644
--- a/verify/thmProvers.ml
+++ b/verify/thmProvers.ml
@@ -21,7 +21,7 @@ let askErgo tasks =
   let outchnl = open_out filename in
   out_ergotasks outchnl tasks;
   close_out outchnl;
-  ignore (Sys.command (Printf.sprintf "alt-ergo -redondance 4 %s" filename));
+  ignore (Sys.command (Printf.sprintf "alt-ergo -redondance 4 -stop 2 %s" filename));
   let s = input_line stdin in
   (* close_in stdin; *)
   print_string ("the result"^s);
diff --git a/verify/toErgosrc.ml b/verify/toErgosrc.ml
index 6850456ca8..d3abd22a3f 100644
--- a/verify/toErgosrc.ml
+++ b/verify/toErgosrc.ml
@@ -178,12 +178,6 @@ else match exp.exp_desc with
             | None -> true) 
 | _ -> false
 
-let is_scrutinee_ergoble exp = match exp.exp_desc with
-| Texp_ident _ -> false
-| Texp_match _ -> false
-| _ -> is_expression_ergoble exp
-
-
 (* HOL, we introduce 
   type ('a, 'b) arrow 
   logic apply : ('a , 'b) arrow , 'a -> 'b *)
@@ -822,6 +816,7 @@ match e0.exp_desc with
     end
    | "=" -> begin match expop_optl_list with 
       | (Some x, _)::(Some y, _)::l -> 
+	  (*
 	  if is_expression_argable x 
 	     then if is_expression_argable y 
 	          then let e1 = expression_to_lexpr x in
@@ -845,10 +840,11 @@ match e0.exp_desc with
 		  let e1 = expression_to_eqlexpr xvar x in
 		  let e2 = expression_to_eqlexpr yvar y in
 		  f_exists x1 t1 (f_exists x2 t2 (f_and (f_and e1 e2) (f_eq xvar yvar)))
-	(*  let e1 = expression_to_lexpr x in
+	    *)
+	  let e1 = expression_to_lexpr x in
 	  let e2 = expression_to_lexpr y in
  	  f_iff (f_eq e1 e2)
-                (f_eq f (mklexpr l0 etrue)) *)
+                (f_eq f (mklexpr l0 etrue)) 
        | _ -> raise Not_primitive
     end
    | "<>" -> begin match expop_optl_list with 
@@ -896,8 +892,8 @@ match e0.exp_desc with
     end 
     | "not" -> begin match expop_optl_list with 
       | (Some x, _)::l -> 
-	  let e1 = expression_to_lexpr x in
- 	  f_eq f (f_not e1)
+	  let e1 = expression_to_eqlexpr f x in
+ 	  f_not e1
       | _ -> raise Not_primitive
     end 
     | _ -> raise Not_primitive
diff --git a/verify/toErgosrc.mli b/verify/toErgosrc.mli
index c930aeaae4..eb41f4f6bc 100644
--- a/verify/toErgosrc.mli
+++ b/verify/toErgosrc.mli
@@ -35,7 +35,6 @@ val type_to_typelogic : loc -> Ident.t * type_declaration -> decl list
 val out_ergotasks : out_channel -> decl list -> unit
 val report_error: Format.formatter -> error -> unit
 val is_expression_ergoble: expression -> bool
-val is_scrutinee_ergoble: expression -> bool
 val bound_vars_to_logic : pattern -> decl list
 val toGoal_beq : expression -> decl
 val toGoal_bneq : expression -> decl
diff --git a/verify/verify.ml b/verify/verify.ml
index 64e96ac8d9..647ced8e62 100644
--- a/verify/verify.ml
+++ b/verify/verify.ml
@@ -14,141 +14,6 @@ type error =
 
 exception Error of Location.t * error
 
-let rec rename_path_ident bvars path id1 id2 = match path with
- | Pident id -> if not(List.mem id bvars) && id = id1
-                then Pident id2
-                else path
- | Pdot (p, s, pos) -> Pdot (rename_path_ident bvars p id1 id2, s, pos)
- | Papply (p1, p2) -> Papply(p1, rename_path_ident bvars p2 id1 id2)
-
-(* subst replace free variables id1 in expr by id2 *)
-let rec subst bound_vars id1 id2 expr = match expr.exp_desc with
- | Texp_ident (path, vd) -> 
-     {expr with exp_desc = Texp_ident (rename_path_ident bound_vars path id1 id2, vd)}
- | Texp_constant (c) -> expr
- | Texp_let (rec_flag, pat_expr_list, e2) -> 
-     let bvars     = let_bound_idents pat_expr_list in
-     let p_e_list  = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) id1 id2 e)) 
-	                   pat_expr_list in
-     let new_e2 = subst bound_vars id1 id2 e2 in
-     {expr with exp_desc = Texp_let (rec_flag, p_e_list, new_e2)}
- | Texp_function (pat_expr_list, ptial) -> 
-     let bvars     = let_bound_idents pat_expr_list in
-     let p_e_list  = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) id1 id2 e)) 
-	                   pat_expr_list in
-     {expr with exp_desc = Texp_function (p_e_list, ptial)}
- | Texp_apply (e1, es) ->
-     let new_e1 = subst bound_vars id1 id2 e1 in
-     let new_es = List.map (fun (e_opt, optl) -> match e_opt with
-                            | Some e -> (Some (subst bound_vars id1 id2 e), optl)
-                            | None -> (None, optl)) es
-     in {expr with exp_desc = Texp_apply (new_e1, new_es)}
- | Texp_match (e0, pat_expr_list, ptial) -> 
-     let new_e0   = subst bound_vars id1 id2 e0 in
-     let bvars    = let_bound_idents pat_expr_list in
-     let p_e_list = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) id1 id2 e)) 
- 	                     pat_expr_list in
-     {expr with exp_desc = Texp_match (new_e0, p_e_list, ptial)} 
- | Texp_try (e1, pat_expr_list) -> 
-     let new_e1   = subst bound_vars id1 id2 e1 in
-     let bvars    = let_bound_idents pat_expr_list in
-     let p_e_list = List.map (fun (p,e) -> (p, subst (bound_vars@bvars) id1 id2 e)) 
- 	                     pat_expr_list in
-     {expr with exp_desc = Texp_try (new_e1, p_e_list)}
- | Texp_tuple (es) -> 
-     let new_es = List.map (subst bound_vars id1 id2) es in
-     {expr with exp_desc = Texp_tuple new_es}
- | Texp_construct (path, cdesc, es) -> 
-     let new_es = List.map (subst bound_vars id1 id2) es in
-     {expr with exp_desc = Texp_construct (path, cdesc, new_es)}
- | Texp_variant (lbl, e_opt) -> 
-     let new_e = match e_opt with
-     | Some e -> Some (subst bound_vars id1 id2 e)
-     | None -> None
-     in {expr with exp_desc = Texp_variant (lbl, new_e)}
- | Texp_record (ldesc_expr_list, e_opt) ->
-     let l_e_list = List.map (fun (p,e) -> (p, subst bound_vars id1 id2 e)) 
- 	                     ldesc_expr_list in
-     {expr with exp_desc = Texp_record (l_e_list, match e_opt with
-     | Some e -> Some (subst bound_vars id1 id2 e)
-     | None -> None)}
- | Texp_field (e, ldesc) -> 
-     let new_e = subst bound_vars id1 id2 e in
-     {expr with exp_desc = Texp_field (new_e, ldesc)}
- | Texp_setfield (e1, ldesc, e2) -> 
-     let new_e1 = subst bound_vars id1 id2 e1 in
-     let new_e2 = subst bound_vars id1 id2 e2 in
-     {expr with exp_desc = Texp_setfield (new_e1, ldesc, new_e2)}
- | Texp_array (es) -> 
-     let new_es = List.map (subst bound_vars id1 id2) es in
-     {expr with exp_desc = Texp_tuple new_es}
- | Texp_ifthenelse (e0, e1, e2_opt) -> 
-     let new_e0 = subst bound_vars id1 id2 e0 in
-     let new_e1 = subst bound_vars id1 id2 e1 in
-     let new_e2 = match e2_opt with
-     | Some e -> Some (subst bound_vars id1 id2 e)
-     | None -> None 
-     in {expr with exp_desc = Texp_ifthenelse (new_e0, new_e1, new_e2)}    
- | Texp_sequence (e1, e2) -> 
-     let new_e1 = subst bound_vars id1 id2 e1 in
-     let new_e2 = subst bound_vars id1 id2 e2 in
-     {expr with exp_desc = Texp_sequence (new_e1, new_e2)}    
- | Texp_while (e1, e2) -> 
-     let new_e1 = subst bound_vars id1 id2 e1 in
-     let new_e2 = subst bound_vars id1 id2 e2 in
-     {expr with exp_desc = Texp_while (new_e1, new_e2)}    
- | Texp_for (id, e1, e2, dflag, e3) ->
-     let new_e1 = subst bound_vars id1 id2 e1 in
-     let new_e2 = subst bound_vars id1 id2 e2 in
-     let new_e3 = subst bound_vars id1 id2 e3 in
-     {expr with exp_desc = Texp_for (id, new_e1, new_e2, dflag, new_e3)}    
-  | Texp_when (e1, e2) -> 
-     let new_e1 = subst bound_vars id1 id2 e1 in
-     let new_e2 = subst bound_vars id1 id2 e2 in
-     {expr with exp_desc = Texp_when (new_e1, new_e2)}    
-  | Texp_send (e, meth) -> 
-     let new_e = subst bound_vars id1 id2 e in
-     {expr with exp_desc = Texp_send (new_e, meth)}    
-  | Texp_new _ -> expr
-  | Texp_instvar _ -> expr
-  | Texp_setinstvar (path1, path2, e) -> 
-     let new_e = subst bound_vars id1 id2 e in
-     {expr with exp_desc = Texp_setinstvar(path1, path2, new_e)}
-  | Texp_override (path1, path_expr_list) -> 
-     let p_e_list = List.map (fun (p,e) -> (p, subst bound_vars id1 id2 e)) 
- 	                      path_expr_list in
-     {expr with exp_desc = Texp_override (path1, p_e_list)}
-  | Texp_letmodule (id, modexpr, e) -> 
-      let new_e = subst bound_vars id1 id2 e in
-      {expr with exp_desc = Texp_letmodule (id, modexpr, new_e)}
-  | Texp_assert (e) -> 
-      let new_e = subst bound_vars id1 id2 e in
-      {expr with exp_desc = Texp_assert(new_e)}
-  | Texp_assertfalse -> expr
-  | Texp_lazy (e) -> 
-      let new_e = subst bound_vars id1 id2 e in
-      {expr with exp_desc = Texp_assert(new_e)}
-  | Texp_object _ -> expr
-  | Texp_pack _ -> expr
-  | Texp_local_contract (c, e) -> 
-      let new_e = subst bound_vars id1 id2 e in
-      {expr with exp_desc = Texp_local_contract(c, new_e)}
-  | Texp_contract (c, e1, e2, e3) -> 
-      let new_e1 = subst bound_vars id1 id2 e1 in
-      let new_e2 = subst bound_vars id1 id2 e2 in
-      let new_e3 = subst bound_vars id1 id2 e3 in
-      {expr with exp_desc = Texp_contract (c, new_e1, new_e2, new_e3)}    
-  | Texp_bad _ -> expr
-  | Texp_unr _ -> expr
-  | Texp_Lambda (ids, e) -> 
-      let new_e = subst bound_vars id1 id2 e in
-      {expr with exp_desc = Texp_Lambda (ids, new_e)}
-  | Texp_App (e1, es) -> 
-      let new_e1 = subst bound_vars id1 id2 e1 in
-      let new_es = List.map (subst bound_vars id1 id2) es in
-      {expr with exp_desc = Texp_App(new_e1, new_es)}
-  | Texp_raise (e) -> expr
-
 (* Translate wrapped expression e |><| c to unwrapped expression 
 val transl_core_contract: 
    Typedtree.contract_declaration list ->         % contract decls in this module
@@ -204,18 +69,18 @@ let rec transl_core_contract env cntr e callee caller =
        *) 
         begin match is_expression_true p with
         | Ptrue ->  e.exp_desc
-	| Pfalse -> callee.exp_desc
         | _ ->
         let new_x = Ident.create "x" in
         let vd = { val_type = e.exp_type; val_kind = Val_reg } in
 	let xe = { e with exp_desc = Texp_ident(Pident new_x, vd) } in
         (* let wrapped_p = contract_id_in_expr env p in 
         let expanded_p = deep_transl_contract env wrapped_p in
-        *)
         let cond = Texp_ifthenelse (subst [] x new_x p, xe, Some callee) in 
+        *)
+        let cond = Texp_ifthenelse (subst [] (Tbl.add x new_x Tbl.empty) p, xe, Some callee) in 
 	Texp_let (Nonrecursive, [(mkpat (Tpat_var new_x) cty, e)], mkexp cond cty) 
         end
-       (* e |>r1,r2<| try {x | p} with [Ei -> booli] 
+        (* e |>r1,r2<| try {x | p} with [Ei -> booli] 
           if (try let x = e in p
               with Contract_exn (f,row,col,bl) -> raise Contract_exn (f,row,col,bl)
                     | Ei .. -> booli
@@ -229,13 +94,10 @@ let rec transl_core_contract env cntr e callee caller =
         (*
         begin match exnop with
         | None -> 
-
         let xe = Texp_ident (Pident x, {val_type = cty; val_kind = Val_reg}) in
         let cond = Texp_ifthenelse (p, mkexp xe cty, Some callee) in
 	Texp_let (Nonrecursive, [(mkpat (Tpat_var x) cty, e)], mkexp cond cty) 
-
         | Some exns -> 
-
 	let letexp = Texp_let (Nonrecursive, [(mkpat (Tpat_var x) cty, e)], p) in
         let ctr_exn = Texp_construct(cexn_path, cexn_cdesc, 
                        [mkexp (Texp_tuple evars) dummy_tuple]) in
@@ -675,19 +537,14 @@ let rec transl_str_contracts contract_flag env strs =
 	   | _ -> false) 
 	     pat_expr_list in *)
          let env1 = add_tasks env (def_to_axioms pre_processed_list) in	 
-	 if depth env = 0 then env1
-         else
-         List.fold_right (fun (p,e) default -> 
+	 List.fold_right (fun (p,e) default -> 
 	     match p.pat_desc with
-	     | Tpat_var (id) when rec_flag = Nonrecursive ->
-		 let new_id   = Ident.rename id in 
-		 let vd       = { val_type = p.pat_type; val_kind = Val_reg } in
-		 let eid      = {exp_desc = Texp_ident(Pident new_id, vd);
-				 exp_type = p.pat_type;
-				 exp_loc  = p.pat_loc;
-				 exp_env  = p.pat_env } in
-		 let env2     = extend_senv default id eid in
-	         extend_denv env2 eid (Inline e)
+	     | Tpat_var (id) ->
+		 begin match rec_flag with
+		 | Nonrecursive -> extend_nonrec_env default id e
+                 | Recursive -> extend_rec_env default id e
+		 | Default -> default
+                 end
 	     | _ -> default) pat_expr_list env1
        with ToErgosrc.Error(loc,err) -> 
 	 ToErgosrc.report_error std_formatter err; env