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

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()