From 0addeb07d4d4036ce34612011a4688f466f80627 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Sat, 10 Jan 2026 00:30:42 +0100
Subject: [PATCH] also swap memory types when swapping memories

---
 src/phl/ecPhlSym.ml |  2 +-
 tests/symmetry.ec   | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 tests/symmetry.ec

diff --git a/src/phl/ecPhlSym.ml b/src/phl/ecPhlSym.ml
index 4868fa478..7d706dcc3 100644
--- a/src/phl/ecPhlSym.ml
+++ b/src/phl/ecPhlSym.ml
@@ -20,7 +20,7 @@ let t_equivS_sym tc =
   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 cond  = f_equivS mtr mtl pr es.es_sr es.es_sl po in
   FApi.xmutate1 tc `EquivSym [cond]
 
 (*-------------------------------------------------------------------- *)
diff --git a/tests/symmetry.ec b/tests/symmetry.ec
new file mode 100644
index 000000000..a2c527c06
--- /dev/null
+++ b/tests/symmetry.ec
@@ -0,0 +1,15 @@
+module M = {
+  proc f() = {
+    var f : int;
+
+    f <- 0;
+  }
+
+  proc g() = {}
+}.
+
+equiv toto: M.g ~ M.f: true ==> ={res}.
+proof.
+proc. symmetry.
+conseq (:true ==> true) (: true ==> f=0).
+abort.