cfold tactic on bdep branch

[bacelar]

The extended cfold tactic on the bdep branch appears too eager in carrying out its work. A faulty example is the following:

module M = {
 proc f(): int = {
   var t, x, y;
   x <- 1;
   y <- 0;
   t <- 2;
   (* 1 0 2 *)
   x <- y;
   y <- t;
   t <- 3;
   (* 0 2 3 *)
   return x;
  }
}.
hoare f_h:
  M.f: true ==> res = 0.
proof.
proc.
(* auto => />. (*This works as expected*) *)
cfold 1; auto => />. (* but not this one! *)

[strub]

cfold in bdep was made in a hurry. I'll have a look.