3 files changed, 8 insertions, 7 deletions
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 1f563c0f..1d7bdbb3 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -757,6 +757,10 @@ namespace Microsoft.Boogie.Simplify {
       //Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
+      VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+      if (v != null) {
+        var = v;
+      }
       return Namer.Lookup(var);
     }
 
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 4a16e6b6..33e622ba 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -597,13 +597,6 @@ namespace Microsoft.Boogie.Z3
           int k = s.IndexOfAny(new char[] { ' ', '}' }, j);
           Contract.Assume(j <= k);
           string id = s.Substring(j, k - j);
-#if IS_THIS_A_GOOD_IDEA
-          // remove any @@-suffix
-          int doubleAt = id.IndexOf("@@");
-          if (doubleAt != -1) {
-            id = id.Substring(0, doubleAt);
-          }
-#endif
           j = k + 1;
           Contract.Assume(!identifierToPartition.ContainsKey(id));  // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
           identifierToPartition.Add(id, zID);
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 9289b5b7..af9668d4 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -295,6 +295,10 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       //Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
+      VCExprVar v = AxBuilder.TryTyped2Untyped(var);
+      if (v != null) {
+        var = v;
+      }
       return Namer.Lookup(var);
     }