From bed8d4a027c635a146911a2ce973046f02a8e719 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 26 Apr 2015 12:57:16 +0100 Subject: Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error --- Source/Provers/SMTLib/SMTLibNamer.cs | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'Source/Provers') 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() -- cgit v1.2.3