fixed problems with datatypes

removed stale contracts in stratified inlining
added test to datatypes

1 files changed, 8 insertions, 5 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 8d4a4256..635280d1 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -660,11 +660,14 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       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('#', '-');

+        if (func is DatatypeSelector) {

+          DatatypeSelector selector = (DatatypeSelector) func;

+          Variable v = selector.constructor.InParams[selector.index];

+          return ExprLineariser.Namer.GetQuotedName(v, v.Name + "#" + selector.constructor.Name);

+        }

+        else if (func is DatatypeMembership) {

+          DatatypeMembership membership = (DatatypeMembership)func;

+          return ExprLineariser.Namer.GetQuotedName(membership, "is-" + membership.constructor.Name);

         }

         else {

           return null;