From 4881964aed5a64c9046a4cbd6d04744a531be536 Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <shaz.qadeer@gmail.com>
Date: Fri, 25 Oct 2024 13:05:00 -0700
Subject: [PATCH] Further cleanup in datatype translation (#977)

---
 Source/Core/AST/Absy.cs           |  4 ----
 Source/VCExpr/ScopedNamer.cs      |  6 +-----
 Test/datatypes/is-cons.bpl        | 12 ++++++++++++
 Test/datatypes/is-cons.bpl.expect |  2 ++
 4 files changed, 15 insertions(+), 9 deletions(-)
 create mode 100644 Test/datatypes/is-cons.bpl
 create mode 100644 Test/datatypes/is-cons.bpl.expect

diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index df0984032..6a3d53f23 100644
--- a/Source/Core/AST/Absy.cs
+++ b/Source/Core/AST/Absy.cs
@@ -699,8 +699,6 @@ public override string ToString()
     {
       return cce.NonNull(Name);
     }
-    
-    public virtual bool MayRename => true;
   }
 
   public class TypeCtorDecl : NamedDeclaration
@@ -1971,8 +1969,6 @@ public DatatypeConstructor(Function func)
       : base(func.tok, func.Name, func.TypeParameters, func.InParams, func.OutParams[0], func.Comment, func.Attributes)
     {
     }
-
-    public override bool MayRename => false;
   }
 
   public class Function : DeclWithFormals
diff --git a/Source/VCExpr/ScopedNamer.cs b/Source/VCExpr/ScopedNamer.cs
index 00d28fead..45b708fc7 100644
--- a/Source/VCExpr/ScopedNamer.cs
+++ b/Source/VCExpr/ScopedNamer.cs
@@ -174,11 +174,7 @@ public virtual string GetName(object thing, string inherentName)
       }
 
       var uniqueInherentName = NextFreeName(thing, inherentName);
-      if (thing is NamedDeclaration namedDeclaration && !namedDeclaration.MayRename)
-      {
-        result = uniqueInherentName;
-      }
-      else if (boogieDeterminedNames.Contains(inherentName))
+      if (boogieDeterminedNames.Contains(inherentName))
       {
         result = uniqueInherentName;
       }
diff --git a/Test/datatypes/is-cons.bpl b/Test/datatypes/is-cons.bpl
new file mode 100644
index 000000000..ced4e462b
--- /dev/null
+++ b/Test/datatypes/is-cons.bpl
@@ -0,0 +1,12 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype X {
+    A'(a: int),
+    B'(b: bool)
+}
+
+procedure P(x: X) {
+    assume x is A';
+    assert !(x is B');
+}
diff --git a/Test/datatypes/is-cons.bpl.expect b/Test/datatypes/is-cons.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/datatypes/is-cons.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors