diff options
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 5 |
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");
}
|