Further cleanup in datatype translation (#977)

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

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;
       }

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');
+}

Test/datatypes/is-cons.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors