diff options
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 7 |
1 files changed, 5 insertions, 2 deletions
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)
|