Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly different syntax in SMT than in Simplify

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 9f16eb5b..4884b44f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -155,6 +155,11 @@ namespace Microsoft.Boogie.SMTLib
       Contract.Requires(f != null);

       string retVal = null;

       retVal = f.FindStringAttribute("bvbuiltin");

+      

+      // It used to be "sign_extend 12" in Simplify, and is "sign_extend[12]" with SMT

+      if (retVal != null && retVal.StartsWith("sign_extend "))

+        return retVal.Replace(" ", "[") + "]";

+

       if (retVal == null) {

         retVal = f.FindStringAttribute("builtin");

       }