From 7ea78551342ff1a1bfe36e2c7f9eaa44a2096a35 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 5 Oct 2011 19:31:21 -0700
Subject: added membership tests

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f008bb88..f4973efd 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -655,10 +655,13 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
-      private string ExtractDatatypeSelector(Function func) {
+      private string ExtractDatatype(Function func) {
         if (QKeyValue.FindBoolAttribute(func.Attributes, "selector")) {
           return func.Name.Remove(func.Name.IndexOf('#'));
         }
+        else if (QKeyValue.FindBoolAttribute(func.Attributes, "membership")) {
+          return func.Name.Replace('#', '-');
+        }
         else {
           return null;
         }
@@ -670,7 +673,7 @@ namespace Microsoft.Boogie.SMTLib
         string printedName;
 
         var builtin = ExtractBuiltin(op.Func);
-        var datatype = ExtractDatatypeSelector(op.Func);
+        var datatype = ExtractDatatype(op.Func);
         if (builtin != null)
           printedName = builtin;
         else if (datatype != null)
-- 
cgit v1.2.3