diff options
Diffstat (limited to 'Source/Provers/SMTLib')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 3ef2039b..40007ab9 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -98,9 +98,14 @@ namespace Microsoft.Boogie.SMTLib return "|" + s + "|";
}
- static string NonKeyword(string s)
+ static string FilterReserved(string s)
{
- if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]))
+ // Note symbols starting with ``.`` and ``@`` are reserved for internal
+ // solver use in SMT-LIBv2 however if we check for the first character
+ // being ``@`` then Boogie's tests fail spectacularly because they are
+ // used for labels so we don't check for it here. It hopefully won't matter
+ // in practice because ``@`` cannot be legally used in Boogie identifiers.
+ if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]) || s[0] == '.')
s = "q@" + s;
// | and \ are illegal even in quoted identifiers
@@ -120,17 +125,17 @@ namespace Microsoft.Boogie.SMTLib public static string QuoteId(string s)
{
- return AddQuotes(NonKeyword(s));
+ return AddQuotes(FilterReserved(s));
}
public override string GetQuotedLocalName(object thingie, string inherentName)
{
- return AddQuotes(base.GetLocalName(thingie, NonKeyword(inherentName)));
+ return AddQuotes(base.GetLocalName(thingie, FilterReserved(inherentName)));
}
public override string GetQuotedName(object thingie, string inherentName)
{
- return AddQuotes(base.GetName(thingie, NonKeyword(inherentName)));
+ return AddQuotes(base.GetName(thingie, FilterReserved(inherentName)));
}
public SMTLibNamer()
|