Fix memory in symmetry tactic

src/phl/ecPhlSym.ml

@@ -9,18 +9,18 @@ open EcSubst
 let t_equivF_sym tc =
   let ef     = tc1_as_equivF tc in
   let ml, mr = ef.ef_ml, ef.ef_mr in
-  let pr     = {ml;mr;inv=(ts_inv_rebind (ef_pr ef) mr ml).inv} in
-  let po     = {ml;mr;inv=(ts_inv_rebind (ef_po ef) mr ml).inv} in
+  let pr     = {ml=mr;mr=ml;inv=(ts_inv_rebind (ef_pr ef) mr ml).inv} in
+  let po     = {ml=mr;mr=ml;inv=(ts_inv_rebind (ef_po ef) mr ml).inv} in
   let cond   = f_equivF pr ef.ef_fr ef.ef_fl po in
   FApi.xmutate1 tc `EquivSym [cond]
 
 (*-------------------------------------------------------------------- *)
 let t_equivS_sym tc =
   let es    = tc1_as_equivS tc in
   let (ml, mtl), (mr, mtr) = es.es_ml, es.es_mr in
-  let pr    = {ml;mr;inv=(ts_inv_rebind (es_pr es) mr ml).inv} in
-  let po    = {ml;mr;inv=(ts_inv_rebind (es_po es) mr ml).inv} in
-  let cond  = f_equivS mtl mtr pr es.es_sr es.es_sl po in
+  let pr    = {mr=ml;ml=mr;inv=(ts_inv_rebind (es_pr es) mr ml).inv} in
+  let po    = {mr=ml;ml=mr;inv=(ts_inv_rebind (es_po es) mr ml).inv} in
+  let cond  = f_equivS mtr mtl pr es.es_sr es.es_sl po in
   FApi.xmutate1 tc `EquivSym [cond]
 
 (*-------------------------------------------------------------------- *)

tests/phl_sym.ec

@@ -0,0 +1,27 @@
+require import AllCore Int.
+
+
+module M = {
+  proc f1(a: int) = {
+    var c : int;
+    c <- a;
+    return c;
+  }
+
+  proc f2(a: int) = {
+    var d;
+    d <@ f1 (a);
+
+    return d;
+  }
+}.
+
+lemma aux (a_: int) : hoare[M.f1 : a_ = a ==> res = a_].
+proof. proc; auto. qed.
+
+lemma test : equiv[M.f2 ~ M.f2 : ={arg} ==> ={res}].
+proc.
+inline {1}.
+symmetry.
+proc change {2} [1-2] : { a0 <- a; }. 
+abort.