1 files changed, 12 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 36df38e3..f008bb88 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -655,14 +655,26 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
+      private string ExtractDatatypeSelector(Function func) {
+        if (QKeyValue.FindBoolAttribute(func.Attributes, "selector")) {
+          return func.Name.Remove(func.Name.IndexOf('#'));
+        }
+        else {
+          return null;
+        }
+      }
+
       public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {
         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
         Contract.Assert(op != null);
         string printedName;
 
         var builtin = ExtractBuiltin(op.Func);
+        var datatype = ExtractDatatypeSelector(op.Func);
         if (builtin != null)
           printedName = builtin;
+        else if (datatype != null)
+          printedName = datatype;
         else
           printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
         Contract.Assert(printedName != null);