diff options
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 3e8a3fc8..ed7beabf 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -157,9 +157,9 @@ namespace Microsoft.Boogie.SMTLib 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(" ", "[") + "]";
+ // It used to be "sign_extend 12" in Simplify, and is "(_ sign_extend 12)" with SMT
+ if (retVal != null && (retVal.StartsWith("sign_extend ") || retVal.StartsWith("zero_extend ")))
+ return "(_ " + retVal + ")";
if (retVal == null) {
retVal = f.FindStringAttribute("builtin");
|