Fix bug in datatype translation (#975)

SMTLib has a convention regarding the syntax for specifying the test for
a variant arm of a datatype. If the variant constructor name is C, a
call to function is-C must be generated. This was not being done
correctly and this PR fixes the problem.

This PR also renames SmtLibNameUtils --> SMTLibNameUtils to match the
convention used for other classes in the SMTLib project.

Source/Provers/SMTLib/SMTLibLineariser.cs

@@ -230,7 +230,7 @@ public string TypeToString(Type t)
         }
         else
         {
-          return SmtLibNameUtils.QuoteId("T@" + s);
+          return SMTLibNameUtils.QuoteId("T@" + s);
         }
       }
     }
@@ -465,7 +465,7 @@ public bool Visit(VCExprQuantifier node, LineariserOptions options)
           wr.Write("\n");
           if (info.qid != null && LibOptions.EmitDebugInformation)
           {
-            wr.Write(" :qid {0}\n", SmtLibNameUtils.QuoteId(info.qid));
+            wr.Write(" :qid {0}\n", SMTLibNameUtils.QuoteId(info.qid));
           }
 
           if (weight != 1)
@@ -775,8 +775,7 @@ public bool VisitFieldAccessOp(VCExprNAry node, LineariserOptions options)
         var op = (VCExprFieldAccessOp)node.Op;
         var constructor = op.DatatypeTypeCtorDecl.Constructors[op.ConstructorIndex];
         Variable v = constructor.InParams[op.FieldIndex];
-        var name = v.Name + "#" + constructor.Name;
-        name = ExprLineariser.Namer.GetQuotedName(v, name);
+        var name = ExprLineariser.Namer.GetQuotedName(v, v.Name);
         WriteApplication(name, node, options);
         return true;
       }
@@ -785,8 +784,8 @@ public bool VisitIsConstructorOp(VCExprNAry node, LineariserOptions options)
       {
         var op = (VCExprIsConstructorOp)node.Op;
         var constructor = op.DatatypeTypeCtorDecl.Constructors[op.ConstructorIndex];
-        var name = "is-" + constructor.Name;
-        name = ExprLineariser.Namer.GetQuotedName(name, name);
+        var constructorName = ExprLineariser.Namer.GetName(constructor, constructor.Name);
+        var name = SMTLibNameUtils.AddQuotes($"is-{constructorName}");
         WriteApplication(name, node, options);
         return true;
       }

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -453,7 +453,7 @@ protected void SendVCOptions()
     protected void SendVCId(string descriptiveName)
     {
       if (this.libOptions.EmitDebugInformation) {
-        SendThisVC("(set-info :boogie-vc-id " + SmtLibNameUtils.QuoteId(descriptiveName) + ")");
+        SendThisVC("(set-info :boogie-vc-id " + SMTLibNameUtils.QuoteId(descriptiveName) + ")");
       }
     }
 

Source/Provers/SMTLib/SmtLibNameUtils.cs

@@ -3,7 +3,7 @@
 
 namespace Microsoft.Boogie.SMTLib
 {
-  public static class SmtLibNameUtils
+  public static class SMTLibNameUtils
   {
 
     public static string QuoteId(string s)
@@ -70,7 +70,7 @@ public static string QuoteId(string s)
     static HashSet<string> reservedSmtWords;
     static bool[] validIdChar;
 
-    static SmtLibNameUtils()
+    static SMTLibNameUtils()
     {
       reservedSmtWords = new HashSet<string>();
       foreach (var w in reservedSmtWordsList)
@@ -112,7 +112,7 @@ static string FilterReserved(string s)
     }
 
 
-    static string AddQuotes(string s)
+    public static string AddQuotes(string s)
     {
       var allGood = true;