summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLibLineariser.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs6
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");